www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - "Verification Corner" videos, contract programming

reply "bearophile" <bearophileHUGS lycos.com> writes:
The Channel9 videos of the "The Verification Corner" (Microsoft 
Research, by Peli de Halleux) are more than two years old, but I 
have missed them so far. They are mostly about usage of the 

(but they also show two other languages). Even if Walter quickly 
found a case where they don't work, the shown verification 
capabilities are interesting and nice.

------------------

"Loop Invariants":
http://channel9.msdn.com/blogs/peli/the-verification-corner-loop-invariants

At 7.56 starts the part on the computer (the part about Hoare 
Triples is often taught at the first year of computer science 
courses).



class method:

modifies m[*];
ensures forall{int i in (0: a.Length); a[i] == i*i*i};

The first line of code (that is part of the post-condition) means 
that at the end of this method the function/method has modified 
every item in the array 'm'. I think we can't express this nicely 
in D contract programming. But even if currently D compilers 

hard to verify that at run-time: you just create a ghost array of 
booleans the same length of 'm' array, and you set its items 
every time an item of 'm' is assigned. And then in the method 
post-condition you test at run-time that this ghost array is 
filled with just true values.

In the second line "ensures" means it's part of the 
post-condition, it becomes something like this in D:

out { foreach (i, ai; a) ai == i ^^ 3; }



invariant{} blocks for loops is better than just writing assert() 
inside a loop because:
- For future static verifiers it will be simple to understand 
that invariant{} blocks are its loop invariant. While assert() 
meaning changes according to the _position_ you put it inside the 
loop. This makes things harder for the verifier.
- Sometimes you have to compute something and then assert it. If 
you put all such computations inside the invariant{} block it's 
easy for the compiler to remove it all in release mode.
- It's simpler for the human programmer to understand that's the 
loop invariant.



is:

while ()
invariant some_condition;
{ loop body... }


loop body itself, this is nice.

I think in D it would become (I don't know if the "body" keyword 
is useful here):

foreach(...) invariant {...} body {...}
for(...) invariant {...} body {...}
while(...) invariant {...} body {...}
do invariant {...} body {...} while(...);

But I think those loop invariants will not be present in lot of 
real life D code.

In the successive minutes he shows that contracts show their true 
power when you have a static verifier in your IDE. Here it's not 
a matter of syntax. Of course, as Walter too as shown, the power 
of that verifier is rather limited.


The whole function he discusses is written in Haskell (but it's 
not in-place, this makes it simpler):

cuber m = map (^3) [0 .. (length m) - 1]

With so short functions and clear syntax it's less easy to 
introduce bugs in the first place :-)

------------------


http://channel9.msdn.com/blogs/peli/the-verification-corner-specifications-in-action-with-specsharp

This is the "Chunker demo", it shows how to write a function that 
chunks a given string into parts.

------------------

"Loop Termination":
http://channel9.msdn.com/blogs/peli/the-verification-corner-loop-termination



It uses this instruction to tell the verifier that the current 
method reads (or is allowed to read?) all fields of the current 
class:
reads *;


At 13.10 he shows the use of ghost variables.

At 15.28 he shows the use of the ==> (implies) operator in a 
normal boolean expression:
return x && (y ==> z && w);

That means:
return x && (!y || (y && z && w));

That means:
return x && (!y || (z && w));


The verification example with the linked list is quite cool. But 
I'd like the static verifier to be able to tell better why he 
can't verify certain assertions, this makes it more simple to 
invent what to feed it to make it happy.

I don't know why the IsAcyclic() function too isn't tagged with 
the "ghost" keyword, as the ListNodes field.

------------------

"Stepwise Refinement":
http://channel9.msdn.com/Blogs/Peli/The-Verification-Corner-Stepwise-Refinement


At 7.22, in what looks yet another language, it shows the <==> 
operator.

It shows array slice syntax as:  a[..x]  a[x..] that's the same 
as a[0..x]  a[x..$] in D.

This video seems boring.

------------------

Bye,
bearophile
Jun 08 2012
parent reply deadalnix <deadalnix gmail.com> writes:
This is awesome.

I wonder what is the method used by the compiler to ensure most of the 
check at compile time. This is really something we can look at to think 
about D's contracts.

Le 08/06/2012 14:57, bearophile a écrit :

 The Channel9 videos of the "The Verification Corner" (Microsoft
 Research, by Peli de Halleux) are more than two years old, but I have
 missed them so far. They are mostly about usage of the static

 show two other languages). Even if Walter quickly found a case where
 they don't work, the shown verification capabilities are interesting and
 nice.

 ------------------

 "Loop Invariants":
 http://channel9.msdn.com/blogs/peli/the-verification-corner-loop-invariants

 At 7.56 starts the part on the computer (the part about Hoare Triples is
 often taught at the first year of computer science courses).



 method:

 modifies m[*];
 ensures forall{int i in (0: a.Length); a[i] == i*i*i};

 The first line of code (that is part of the post-condition) means that
 at the end of this method the function/method has modified every item in
 the array 'm'. I think we can't express this nicely in D contract
 programming. But even if currently D compilers don't have static

 run-time: you just create a ghost array of booleans the same length of
 'm' array, and you set its items every time an item of 'm' is assigned.
 And then in the method post-condition you test at run-time that this
 ghost array is filled with just true values.

 In the second line "ensures" means it's part of the post-condition, it
 becomes something like this in D:

 out { foreach (i, ai; a) ai == i ^^ 3; }



 invariant{} blocks for loops is better than just writing assert() inside
 a loop because:
 - For future static verifiers it will be simple to understand that
 invariant{} blocks are its loop invariant. While assert() meaning
 changes according to the _position_ you put it inside the loop. This
 makes things harder for the verifier.
 - Sometimes you have to compute something and then assert it. If you put
 all such computations inside the invariant{} block it's easy for the
 compiler to remove it all in release mode.
 - It's simpler for the human programmer to understand that's the loop
 invariant.




 while ()
 invariant some_condition;
 { loop body... }


 body itself, this is nice.

 I think in D it would become (I don't know if the "body" keyword is
 useful here):

 foreach(...) invariant {...} body {...}
 for(...) invariant {...} body {...}
 while(...) invariant {...} body {...}
 do invariant {...} body {...} while(...);

 But I think those loop invariants will not be present in lot of real
 life D code.

 In the successive minutes he shows that contracts show their true power
 when you have a static verifier in your IDE. Here it's not a matter of
 syntax. Of course, as Walter too as shown, the power of that verifier is
 rather limited.


 The whole function he discusses is written in Haskell (but it's not
 in-place, this makes it simpler):

 cuber m = map (^3) [0 .. (length m) - 1]

 With so short functions and clear syntax it's less easy to introduce
 bugs in the first place :-)

 ------------------


 http://channel9.msdn.com/blogs/peli/the-verification-corner-specifications-in-action-with-specsharp


 This is the "Chunker demo", it shows how to write a function that chunks
 a given string into parts.

 ------------------

 "Loop Termination":
 http://channel9.msdn.com/blogs/peli/the-verification-corner-loop-termination




 It uses this instruction to tell the verifier that the current method
 reads (or is allowed to read?) all fields of the current class:
 reads *;


 At 13.10 he shows the use of ghost variables.

 At 15.28 he shows the use of the ==> (implies) operator in a normal
 boolean expression:
 return x && (y ==> z && w);

 That means:
 return x && (!y || (y && z && w));

 That means:
 return x && (!y || (z && w));


 The verification example with the linked list is quite cool. But I'd
 like the static verifier to be able to tell better why he can't verify
 certain assertions, this makes it more simple to invent what to feed it
 to make it happy.

 I don't know why the IsAcyclic() function too isn't tagged with the
 "ghost" keyword, as the ListNodes field.

 ------------------

 "Stepwise Refinement":
 http://channel9.msdn.com/Blogs/Peli/The-Verification-Corner-Stepwise-Refinement



 At 7.22, in what looks yet another language, it shows the <==> operator.

 It shows array slice syntax as: a[..x] a[x..] that's the same as a[0..x]
 a[x..$] in D.

 This video seems boring.

 ------------------

 Bye,
 bearophile
Jun 12 2012
parent reply "bearophile" <bearophileHUGS lycos.com> writes:
deadalnix:


 I wonder what is the method used by the compiler to ensure most 
 of the check at compile time.


It uses Z3 and Boogie:
http://rise4fun.com/

Bye,
bearophile
Jun 12 2012
parent reply deadalnix <deadalnix gmail.com> writes:
Le 12/06/2012 14:55, bearophile a écrit :

 deadalnix:


 I wonder what is the method used by the compiler to ensure most of the
 check at compile time.


 It uses Z3 and Boogie:
 http://rise4fun.com/

 Bye,
 bearophile


OK, but how does that work internally :D Some example are 
straightforward, but others are really black magic to me.
Jun 12 2012
parent reply "bearophile" <bearophileHUGS lycos.com> writes:
deadalnix:


 OK, but how does that work internally :D


http://research.microsoft.com/en-us/um/redmond/projects/z3/

In that page there are links to papers too.

Bye,
bearophile
Jun 12 2012
parent reply deadalnix <deadalnix gmail.com> writes:
Le 12/06/2012 15:52, bearophile a écrit :

 deadalnix:


 OK, but how does that work internally :D


 http://research.microsoft.com/en-us/um/redmond/projects/z3/

 In that page there are links to papers too.

 Bye,
 bearophile


Thank you very much. I was turning endlessly in the website without 
finding that. I now have some stuffs to read.
Jun 12 2012
parent "Tobias Pankrath" <tobias pankrath.net> writes:
 Thank you very much. I was turning endlessly in the website 
 without finding that. I now have some stuffs to read.


As far as I can tell, Z3 is an SMT solver (Satisfiability Modulo 
Theories), which is a SAT Solver an steroids.
Jun 12 2012