Simple loop example for Hoare logic

joom · joom · commit e9e3c41e856a · 2022-05-18T13:03:25.000-04:00
diff --git a/examples/⊢ {i = 0} while (i 3) do (i = i + 1) {i = 3}.proof b/examples/⊢ {i = 0} while (i 3) do (i = i + 1) {i = 3}.proof
@@ -0,0 +1,2 @@
+/* Proof for ⊢ {i = 0} while (i < 3) do (i := i + 1) {i = 3} */
+new Consequence(new Z3Rule(new Sequent([new Equal(new TermVar("i"), new TermInt(0))], [new LeqThan(new TermVar("i"), new TermInt(3))])), new Loop(new ConsequenceNoPost(new Z3Rule(new Sequent([new And(new LeqThan(new TermVar("i"), new TermInt(3)), new LessThan(new TermVar("i"), new TermInt(3)))], [new LeqThan(new AddTerms(new TermVar("i"), new TermInt(1)), new TermInt(3))])), new Assignment(new HoareTriple(new LeqThan(new AddTerms(new TermVar("i"), new TermInt(1)), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1))), new LeqThan(new TermVar("i"), new TermInt(3)))), new HoareTriple(new And(new LeqThan(new TermVar("i"), new TermInt(3)), new LessThan(new TermVar("i"), new TermInt(3))), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1))), new LeqThan(new TermVar("i"), new TermInt(3)))), new HoareTriple(new LeqThan(new TermVar("i"), new TermInt(3)), new CmdWhile(new LessThan(new TermVar("i"), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1)))), new And(new LeqThan(new TermVar("i"), new TermInt(3)), new Not(new LessThan(new TermVar("i"), new TermInt(3)))))), new Z3Rule(new Sequent([new And(new LeqThan(new TermVar("i"), new TermInt(3)), new Not(new LessThan(new TermVar("i"), new TermInt(3))))], [new Equal(new TermVar("i"), new TermInt(3))])), new HoareTriple(new Equal(new TermVar("i"), new TermInt(0)), new CmdWhile(new LessThan(new TermVar("i"), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1)))), new Equal(new TermVar("i"), new TermInt(3))))

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+/* Proof for ⊢ {i = 0} while (i < 3) do (i := i + 1) {i = 3} */`
	`2`	+new Consequence(new Z3Rule(new Sequent([new Equal(new TermVar("i"), new TermInt(0))], [new LeqThan(new TermVar("i"), new TermInt(3))])), new Loop(new ConsequenceNoPost(new Z3Rule(new Sequent([new And(new LeqThan(new TermVar("i"), new TermInt(3)), new LessThan(new TermVar("i"), new TermInt(3)))], [new LeqThan(new AddTerms(new TermVar("i"), new TermInt(1)), new TermInt(3))])), new Assignment(new HoareTriple(new LeqThan(new AddTerms(new TermVar("i"), new TermInt(1)), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1))), new LeqThan(new TermVar("i"), new TermInt(3)))), new HoareTriple(new And(new LeqThan(new TermVar("i"), new TermInt(3)), new LessThan(new TermVar("i"), new TermInt(3))), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1))), new LeqThan(new TermVar("i"), new TermInt(3)))), new HoareTriple(new LeqThan(new TermVar("i"), new TermInt(3)), new CmdWhile(new LessThan(new TermVar("i"), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1)))), new And(new LeqThan(new TermVar("i"), new TermInt(3)), new Not(new LessThan(new TermVar("i"), new TermInt(3)))))), new Z3Rule(new Sequent([new And(new LeqThan(new TermVar("i"), new TermInt(3)), new Not(new LessThan(new TermVar("i"), new TermInt(3))))], [new Equal(new TermVar("i"), new TermInt(3))])), new HoareTriple(new Equal(new TermVar("i"), new TermInt(0)), new CmdWhile(new LessThan(new TermVar("i"), new TermInt(3)), new CmdAssign(new TermVar("i"), new AddTerms(new TermVar("i"), new TermInt(1)))), new Equal(new TermVar("i"), new TermInt(3))))