"Verification Corner" videos, contract programming

[deadalnix]

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