In this article, I’ll look at a common problem one encounters when verifying programs: namely, writing loop invariants. In short, a loop invariant is a property of the loop which:
- holds on entry to the loop;
- holds after the loop body is executed;
- holds when the loop finishes.
Loop invariants can be tricky to get right but, without them, the verification will probably fail. Let’s consider a very simple example:
define nat as int where $ >= 0
nat counter(int count):
i = 0
while i < count:
i = i + 1
return i
This program does not verify. In order to get it to verify, we need to add a loop invariant. The need for loop invariants arises from Hoare’s rule for while-loops. The key issue is that the verifier does not know anything about any variable modified within a loop, other than what the loop condition and/or invariant states.
In our example above, the loop condition only tells us that i < count during the loop, and that i >= count after the loop (in fact, we can be more precise here but the verifier cannot). Knowing that i >= count is not enough to prove the function’s post-condition (i.e. that i >= 0). This is because count is an arbitrary int which, for example, may be negative.
Therefore, to get our example to verify, we need a loop invariant that explicitly states i cannot be negative:
nat counter(int count):
i = 0
while i < count where i >= 0:
i = i + 1
return i
The loop invariant is specified on the while loop with the where keyword. In this case, it simply states that i is always >=0. Whilst this might seem obvious to us, it is unfortunately not so obvious to the verifier! In principle, we could employ a simple form of static analysis to infer this loop invariant (although, currently, Whiley does not do this). Unfortunately, in general, we will need to write loop invariants ourselves.
To explore a slightly more complex example, I’ve put together a short video which illustrates using Whiley to verify a program which sums a list of natural numbers:
Finally, if you’re interested in trying this out for yourself, the easiest way to install Whiley is through the Eclipse Plugin. Have fun!
Hello!
I think Whiley is a really interesting language. I love such concepts as verifying programs and deriving algorithms from specifications. Is it possible to define a type with Whiley in an algebraic specification style? Example:
functions
new : stack;
push : element * stack -> stack;
empty : stack -> boolean;
pop : stack -> stack;
top : stack -> element;
axioms
empty( new ) = true
empty( push(x,s) ) = false
top( push(x,s) ) = x
pop( push(x,s) ) = s
preconditions
pre: pop( s : stack ) = not empty(s)
pre: top( s : stack ) = not empty(s)
end
Hi Jose,
At the moment, specifying global axioms as you have is not supported. I do plan to add that in the future. In general, you can define a data type like so:
define Stack as [int] // stack is a list of ints define EmptyStack as Stack where |$| == 0 define NonEmptyStack as Stack where |$| > 0 EmptyStack Empty(): return [] NonEmptyStack push(Stack stack, int element): return stack + element Stack pop(NonEmptyStack stack) ensures |$|==|stack|-1: last = |stack| - 1 return stack[0..last] int top(NonEmptyStack stack): last = |stack| - 1 return stack[last]That covers of some of axioms you specified, but not all. For example, showing that
pop(push(s,x)) == sis not possible yet.Hello Dave,
It was very kind of you to reply so fast!
I’m sure It will be a very useful feature.
Thanks for the help. The axiom
‘pop(push(s,x)) == s’
is actually the difficult one. Meyer, in his OOSC book, does not implement it with assertions within the STACK[G] class.
I’ve installed ‘Eclipse IDE for Java Developers 32 bits, Version: Juno Service Release 1, Build id: 20120920-0800′ and, when I tried to install the Whiley plugin I found the following error message:
‘An error occurred while collecting items to be installed
session context was:(profile=epp.package.java, phase=org.eclipse.equinox.internal.p2.engine.phases.Collect, operand=, action=).
Artifact not found: http://whiley.org/eclipse/plugins/wyclipse_0.0.14.jar.
http://whiley.org/eclipse/plugins/wyclipse_0.0.14.jar
Artifact not found: http://whiley.org/eclipse/features/wyclipse.feature_0.1.6.jar.
http://whiley.org/eclipse/features/wyclipse.feature_0.1.6.jar‘
Can you help me? Thanks in advance.
Kind regards,
Jose
Hi Jose,
Interesting, well I haven’t actually tested the plugin on Juno yet. So, that might the problem … I’ll investigate. Also, you can download the WDK and run the compiler from the command-line. You need to provide a command-line switch to get verification to work. e.g.
Hi Jose,
Ok, I tried to install it on Juno at work and yes I see the same problem. So, I’ll try to figure it out now …
D
Hi Jose,
Ok, looks like it was a permissions problem. It has now installed successfully on my Juno Eclipse release at work (so you should try the install again).
To get started once installed, you need to create a “Whiley Project”. Go to “File->New Project” then scroll down to the bottom of the available project wizards and you should see the Whiley folder, and the new project wizard in there. Once you’ve created a Whiley Project, then add a Whiley Module to the src folder. At this point, you should be good to go. Note that the compiler only runs when you save the file, and it is a little slow…
Let me know how you go!
Hi Dave!
Thank you again! I’ve been able to install the plugin on Juno. I have my Whiley project and module ‘HelloWorld.whiley’ (inside a folder of name ‘foo’) with the following source code:
package foo;
import * from whiley.lang.*
void ::main(System.Console sys):
sys.out.println(“Hello World”)
The problem is tryint to launch the program. I right-click on the Whiley module and select “Run Configurations”. From there, I create a “Whiley Application” configuration and associate it with my project.
But I don’t know which is the ‘Main class’ or Main Type. I’ve tried with ‘System’, ‘HelloWorld’ and ‘foo’. Also with ‘main’ and ‘Main’ and it doesn’t work.
It should be something easy, I suppose.
Hey Jose,
Ah, well … that’s not a bug. It’s a feature. The eclipse plugin is sketchy, but is just enough to show verification working.
In fact, I can’t get the “hello world” example to compile under Eclipse [because the compiler cannot find the Whiley standard library].
If you want to run code, you’ll need to use the WDK for now (sorry).
Hi Dave,
I’ve been trying to compile and run the ‘HelloWorld’ example with the WDK (release (0.3.18) on Ubuntu. When I try to compile, I get the following error message:
wyjc HelloWorld.whiley
/home/josemarivg/Whiley/wdk-v0.3.18/bin/wyjc: line 32: /home/josemarivg/Whiley/wdk-v0.3.18/bin/../bin/wy_common.bash: No such file or directory
Error: Could not find or load main class wyjc.WyjcMain
I opened the ‘/wdk-v0.3.18/bin/wyjc’ and saw a reference to a ‘wy_common.bash’ file but, when I unpacked the .tgz, I didn’t find anyone.
Thanks! Regards,
Jose
Hey Jose,
Ah, a catalogue of teething problems … but thanks for being so patient!! In fact, someone else also reported this issue already, and I have corrected it in the download for v0.3.18. I’m thinking maybe you orginally downloaded the wdk-v0.3.18.tgz a while ago when you first saw the blog post? In which case, downloading it again should resolve the problem (which basically was me forgetting for various reasons to include that file in the release).
Just in case that doesn’t help, you can get the file from here and then just place it into the
bin/directory of the wdk.My pleasure, Dave. I’ve downloaded again the WDK. I’m trying to use it now on a Windows machine with Cygwin installed (I’m not at home). I’ve set the PATH the environment variable to point to bin/ directory where the scripts are. And when I execute the compiler (‘wyjc’ command), I get the error:
Library ‘wyjc’ not found
But, well, in the lib directory I can see all the required jars.
Hey Jose,
You know what, scrap all that I said below. Looking again at what you said, I think you’ve configured everything correctly. This is a problem with the
wy_common.bashfile. I didn’t actually write that file — an RA did and I know he didn’t test on cygwin. That must be the problem …D
Ok, sounds like something is wrong with the configuration ofPATH. Depending on how comfortable with the UNIX command-line you are, You can try a few things from a Cygwin X-Term:1) Change to the wdk directory, e.g. with something like
cd wdk-v0.3.182) Then try executing the command
bin/wyjc -help. If this prints usage information, then you can runwyjcfrom there usingbin/wyjc(basically this avoids thePATHissue by giving an explicit location forwyjc).3) If that isn’t helping, or you want to figure out what’s up with the
PATHvariable, then try executing this from the command-line:echo $PATH. This will tell you what the current setting forPATHis. Check that it includes the location you specified, and:* If
PATHdoesn’t contain the location you added, then let’s try making sure you’re in a proper shell. Run the commandbash, which should appear to do little except change the nature of the command-line. Then, runecho $PATHagain and see if what you want is there. If it is, try runningwyjcand see if it works.* If
PATHdid contain the location you were expecting, then it’s probably misconfigured somehow. You probably need to show me the contents of that variable before I can diagnose.Anyway, it’s difficult to give you more explicit instructions because it depends on a lot of UNIX stuff, and how exactly your environment is configured. If you’re not too comfortable with the UNIX command-line, then perhaps you know someone who is?
Eitherway, let me know how you get on …
I’m installing Cygwin now, and I’ll have to debug the problem … will get back to you on that. In the meantime, you can run directly using this command (from within wdK directory):
java -cp "lib\wyc-v0.3.17.jar;lib\wyjc-v0.3.18.jar; lib\wyil-v0.3.18.jar;lib\wyone-v0.3.18.jar" wyjc.WyjcMain -wp lib\wyrt-v0.3.18.jar hello-world.whiley(replace
hello-world.whileywith whatever whiley file you want to compile. Additionally, to enable verification to you need to supply the-X verification:enable=trueswitch before-wp ....Hi Jose,
Ok, I have a temporary fix for you. If you change to the wdk directory, then execute
bin/wyjcit seems to work on my Cygwin install. I.e. something like this:Not quite sure why it doesn’t work in conjunction with the
PATHvariable, as that does work OK under UNIX. Hmmm, anyway … thanks for pointing out the problems!! I definitely need to test more on Cygwin … which I used to do a lot, but since I got a Mac Book it’s fallen by the wayside …Dave
Hi Jose,
Ok, fixed but I’m not going to update the
wdk-v0.3.18download, and instead I’ll put the fix in the next release (assuming I don’t find any further problems with it). You can manually edit the file in question (bin/wy_common.bash). Early on it readscygpath -pw $LIBDIR, which should becomecygpath -m $LIBDIR.You can also download the raw file from here:
https://raw.github.com/DavePearce/Whiley/devel/bin/wy_common.bash
Please let me know if that works!!
[...] idea of a loop invariant. For some general background on writing loop invariants in Whiley, see my previous post. To recap the main points, here’s a simple function which requires a loop invariant to [...]
[...] entry to the loop. This is quite a departure from the way we think about verifying While loops (see here and here for more on that). In fact, we could still require that the loop invariant holds on entry [...]