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
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
