Hoare Logic

Sample Code

• There can be only 26 variables(int and bool - a to z). Any type of assignment is possible after declaration only
• There are 26 integer arrays - A to Z
• Two dataypes int and bool
• pre stands for precondition. post for post condition and inv for loop invariant
• @ stands for universal quantifier and # stands for existensial quantifier
• Datatypes of free variables need to be mentioned. Arrays are already of int type

Installation

Install z3 solver

make
./a.out < tests/copy.txt

Valid Hoare Triples

pre true;
A[0] = 1;
post A[0]==1;

---

pre {
	int n;
	n>0;
}
n=5;
A[3] = n;
post A[3] == 5;

---

pre {
	int x;
	int y;
	(x>0) && (y>0)&& (x>=y);
}

int r;
r = x;

inv (x>0) && (y>0)&& (x>=y) && (r>=0) && (r<=x);
while(r>=y){
 	r = r - y;
}

post (x>0) && (y>0)&& (x>=y) && (r>=0) && (r<y) && (r>=0) && (r<=x);

---

pre {
	int x;
	(x>0); 
}

if (x%2 == 0){
	x = x+1;
}
else {
	x = x+2;
}

post x%2 == 1;

Invalid Hoare triples

pre true;
A[0] = 1;
post A[0]==2;

---

pre {
	int i;
	i<0;
}
post i>0;

Check tests for more examples.

Output

• Proves the correctness of hoare-triple. Provides counter-example if fails.

Reference

• https://www.cs.cmu.edu/~aldrich/courses/654-sp07/slides/7-hoare.pdf
• http://ftp.mozgan.me/Compiler_Manuals/LexAndYaccTutorial.pdf
• https://github.com/Z3Prover/z3