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

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

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

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.

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

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.

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