]> begriffs open source - acsl-example/commit
begriffs.com / projects / acsl-example / commit
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ff5c5e) | patch
Incomplete coq proofs from why3
authorJoe Nelson <joe@begriffs.com>
Mon, 8 Sep 2025 01:49:48 +0000 (20:49 -0500)
committerJoe Nelson <joe@begriffs.com>
Mon, 8 Sep 2025 01:49:48 +0000 (20:49 -0500)
commit230968fb36fc68f4a892a739ba5962bbd2952474
treec0570a804a68526307b532575a01365e6881bdeftree | snapshot
parent3ff5c5e63c54a146da580223d80b95e84946acd1commit | diff
Incomplete coq proofs from why3
21 files changed:
proof/find3/interactive/find3_assert_found.v [new file with mode: 0644] blob
proof/find3/interactive/find3_loop_invariant_bound_preserved.v [new file with mode: 0644] blob
proof/find3/interactive/find3_loop_invariant_not_found_established.v [new file with mode: 0644] blob
proof/find3/interactive/find3_loop_invariant_not_found_preserved.v [new file with mode: 0644] blob
proof/find3/interactive/find3_loop_variant_decrease.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Empty.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Extend.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Hit.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Increasing.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Limit.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Lower.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_MissHit.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_MissMiss.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_NoneEqual.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_ResultEqual.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_ResultNoneEqual.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_SomeEqual.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_Upper.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_Find_WeaklyIncreasing.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_NoneEqual_NotSomeEqual.v [new file with mode: 0644] blob
proof/find3/interactive/lemma_NotSomeEqual_NoneEqual.v [new file with mode: 0644] blob
provably correct C with weakest preconditions