Hello,
I'm Yang. I'm student & I have a small research about Software Verification, I search on Internet & find Z3 prover/solver. I think it is tool that i need. But in a short time, I can't handle all of API of Z3, so I have a confuse problem:
How do I write some structure such as if....else; switch...case; while; for; ... in Z3?
And how I write a programe to check a small program that is right or wrong?
Example: I have a program named "greaterValue", it return a greater value among two value (int a, int b). But I have wrong code as:
int greaterValue(int a, int b){ int result; if(a>=b) result = a+10; // the right code must be: result = a; else result = b; return result;}
//The correct expression for this program: (((x>=y)&&(max==x))||((x<y)&&(max==y)))
How I use Z3 to recognize this code is wrong & generate counter-example to illustrate.
Thank you very much.
Yang. H
more info: I want to write code with .NET API
Dear Yang,
It sounds like you want to perform program verification. There are several existing tools that build on top of Z3 to perform program verification. In particular, try out Spec#: http://research.microsoft.com/en-us/projects/specsharp/.
You will also find quite extensive documentation on how formulas (verification conditions) are extacted from imperative/object-oriented programs. When done for realistic settings, this is a considerable task.
Regards,
Nikolaj
Hello Nikolaj,
Thank you very muck about your respond. But my assignment require me write code using Z3 API for C (.NET). I need some documentation about how to write some struct such as if....else; loop structure such as: for; while, ...
Can you give the documentation about that? And have you any example to demo these struct.
Thank you
Hi Nikolaj,
Thank you very much about your respond. But my assignment requires me to use Z3, so I need some documentation about how to use structures such as if…else; for; while on Z3.
Can you give me the document about these structures? And give me some examples about that?
Thank you,
hello Nikolaj,
How can I represent inference rule like the example below by using Z3?
-------- example represent in Prolog--------
odd(1).odd(X):- Y is X-2, odd(Y)
=======run goal===============odd(9) => yes
---------------------------------
Thanks
You suggest you are using Horn clauses. Horn clauses are special cases of first-order formulas, where there is at most one positive disjunct.
So in SMT-lIB syntax:
:assumption (odd 1)
:assumption (forall (x Int) (implies (odd (- x 2)) (odd x))
can you give me the solution for this snip code in C/.Net API syntax?
Thank you very much
Yang.H