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
