"Verification Corner" videos, contract programming

[bearophile]

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 verification of contract programming of Spec# language 
(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).


At 9.45 Peli de Halleux shows two lines of Spec# code inside a 
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 
don't have static verifiers (like Spec# has), it's not too much 
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; }


At 10.22 it shows that Spec# has loop invariants. In D having 
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.


At 10.22 he shows that in Spec# the syntax for the loop invariant 
is:

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

So in Spec# the loop invariant is written before and outside the 
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 :-)

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

"Specifications in Action with Spec#":
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

Here he uses the Dafny language, similar to C#.

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