Commit graph

25 commits

Author SHA1 Message Date
08bad28fa9 Update README 2017-12-08 03:34:05 +01:00
b9fcc3f5ee Remove a few admitted points for certain_termination 2017-12-08 03:17:55 +01:00
3888b62c6a Annotate while with invariants in the language 2017-12-07 20:26:25 +01:00
4f15160760 Implement and prove wps 2017-12-07 20:02:46 +01:00
c161437c7f Totally prove wp correctness 2017-12-07 20:02:46 +01:00
cd467dc8b0 Revert before introduction of option Assert
This mostly reverts commit c2c58119be.
The theorems will be slightly different and should be way cleaner.
2017-12-07 20:02:46 +01:00
260ac05c6e Progress towards proved wp with option Assert 2017-12-07 20:02:18 +01:00
c2c58119be Finish proving wp_correctness 2017-12-07 15:52:53 +01:00
27389f132f Prove good part of wp_correctness_provable 2017-12-07 01:09:29 +01:00
908bed1331 Reindent consistently bullets 2017-12-06 22:19:17 +01:00
5dfc412c10 Prove 2.3 assuming 1.6 2017-12-06 22:01:35 +01:00
3ed5ef8ea4 Nearly prove Th2.3, assuming 1.6 and one small subgoal 2017-12-06 15:19:57 +01:00
82eb5f2189 Define function wp, state wp_correctness 2017-12-06 11:32:57 +01:00
2431f66b07 Stash th2.3 for now 2017-12-06 11:17:17 +01:00
c49f9d3f6e Th2.3: prove error case of transitivity 2017-12-06 10:37:35 +01:00
55eef82c54 Th2.3: prove If rule 2017-12-06 01:15:10 +01:00
93336c705e Prove Th2.3 up to consequence 2017-12-05 18:18:02 +01:00
06f655c1c1 Rewrite hoare_provability inductively 2017-12-05 14:19:43 +01:00
d1b62ad2b5 Modify notation, state theorem 2.3 2017-12-05 00:27:35 +01:00
7e2c2e08dc Axiomatize Hoare provability |- 2017-12-04 23:59:25 +01:00
90ca9bc5bb Implement most operators on assertions 2017-11-16 15:22:35 +01:00
98286d1ad8 Axiomatize CPOs, begin work on interpretation 2017-11-09 14:50:33 +01:00
94bc771b16 Update deadlines 2017-10-26 14:43:31 +02:00
23ca813c8c Define instructions 2017-10-19 15:25:03 +02:00
653e155f41 Initial commit 2017-10-19 14:53:14 +02:00