boogie
by Microsoft Research
Is this property always true?
Ask boogie!
procedure F(n: int) returns (r: int) ensures 100 < n ==> r == n - 10; // This postcondition is easy to check by hand ensures n <= 100 ==> r == 91; // Do you believe this one is true? { if (100 < n) { r := n - 10; } else { call r := F(n + 11); call r := F(r); } }
home
permalink
More samples
Find
DutchFlag
Bubble
About Boogie - Intermediate Verification Language
Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages.
home
tutorials
project map
live
developer
about
© 2012 Microsoft Corporation -
terms of use
-
privacy