Commit graph

Select branches

Hide pull requests

MEH

certain_termination_wip

master

submitted

no_invariants

q6

submit

Mono Color

• 08bad28fa9 Update README master submit submitted Théophile Bastian 2017-12-08 03:32:53 +0100
• f2f17d77e2 [WIP] Try proving certain_termination certain_termination_wip Théophile Bastian 2017-12-08 03:18:39 +0100
• b9fcc3f5ee Remove a few admitted points for certain_termination Théophile Bastian 2017-12-08 03:17:55 +0100
• ab75f25317 MEH MEH Théophile Bastian 2017-12-07 23:59:30 +0100
• 3888b62c6a Annotate while with invariants in the language Théophile Bastian 2017-12-07 20:26:25 +0100
• 4f15160760 Implement and prove wps no_invariants Théophile Bastian 2017-12-07 20:00:36 +0100
• c161437c7f Totally prove wp correctness q6 Théophile Bastian 2017-12-07 18:09:59 +0100
• cd467dc8b0 Revert before introduction of option Assert Théophile Bastian 2017-12-07 16:55:47 +0100
• 260ac05c6e Progress towards proved wp with option Assert Théophile Bastian 2017-12-07 16:24:27 +0100
• c2c58119be Finish proving wp_correctness Théophile Bastian 2017-12-07 15:52:53 +0100
• 27389f132f Prove good part of wp_correctness_provable Théophile Bastian 2017-12-07 01:09:29 +0100
• 908bed1331 Reindent consistently bullets Théophile Bastian 2017-12-06 22:19:17 +0100
• 5dfc412c10 Prove 2.3 assuming 1.6 Théophile Bastian 2017-12-06 20:02:17 +0100
• 3ed5ef8ea4 Nearly prove Th2.3, assuming 1.6 and one small subgoal Théophile Bastian 2017-12-06 15:19:57 +0100
• 82eb5f2189 Define function wp, state wp_correctness Théophile Bastian 2017-12-06 11:32:57 +0100
• 2431f66b07 Stash th2.3 for now Théophile Bastian 2017-12-06 11:17:17 +0100
• c49f9d3f6e Th2.3: prove error case of transitivity Théophile Bastian 2017-12-06 10:37:35 +0100
• 55eef82c54 Th2.3: prove If rule Théophile Bastian 2017-12-06 01:15:10 +0100
• 93336c705e Prove Th2.3 up to consequence Théophile Bastian 2017-12-05 16:15:40 +0100
• 06f655c1c1 Rewrite hoare_provability inductively Théophile Bastian 2017-12-05 14:19:43 +0100
• d1b62ad2b5 Modify notation, state theorem 2.3 Théophile Bastian 2017-12-05 00:27:35 +0100
• 7e2c2e08dc Axiomatize Hoare provability |- Théophile Bastian 2017-12-04 23:37:38 +0100
• 90ca9bc5bb Implement most operators on assertions Théophile Bastian 2017-11-16 15:22:35 +0100
• 98286d1ad8 Axiomatize CPOs, begin work on interpretation Théophile Bastian 2017-11-09 14:50:33 +0100
• 94bc771b16 Update deadlines Théophile Bastian 2017-10-26 14:43:31 +0200
• 23ca813c8c Define instructions Théophile Bastian 2017-10-19 15:25:03 +0200
• 653e155f41 Initial commit Théophile Bastian 2017-10-19 14:53:14 +0200