# Understanding Loop Invariants in Whiley

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:

1. holds on entry to the loop;
2. holds after the loop body is executed;
3. 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!

### 17 comments to Understanding Loop Invariants in Whiley

• José María

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)) == s` is not possible yet.

• José María

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=).
http://whiley.org/eclipse/plugins/wyclipse_0.0.14.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.

```bin/wyjc -X verification:enable=true file.whiley
```
• 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!

• José María

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

• José María

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.

• José María

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:

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.bash` file. 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 of `PATH`. 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.18`

2) Then try executing the command `bin/wyjc -help`. If this prints usage information, then you can run `wyjc` from there using `bin/wyjc` (basically this avoids the `PATH` issue by giving an explicit location for `wyjc`).

3) If that isn’t helping, or you want to figure out what’s up with the `PATH` variable, then try executing this from the command-line: `echo \$PATH`. This will tell you what the current setting for `PATH` is. Check that it includes the location you specified, and:

* If `PATH` doesn’t contain the location you added, then let’s try making sure you’re in a proper shell. Run the command `bash`, which should appear to do little except change the nature of the command-line. Then, run `echo \$PATH` again and see if what you want is there. If it is, try running `wyjc` and see if it works.

* If `PATH` did 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.whiley` with whatever whiley file you want to compile. Additionally, to enable verification to you need to supply the `-X verification:enable=true` switch before `-wp ...`.

• Hi Jose,

Ok, I have a temporary fix for you. If you change to the wdk directory, then execute `bin/wyjc` it seems to work on my Cygwin install. I.e. something like this:

```~\$ cd wdk-v0.3.18
~/wdk-v0.3.18\$ bin/wyjc somefile.whiley
```

Not quite sure why it doesn’t work in conjunction with the `PATH` variable, 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.18` download, 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 reads `cygpath -pw \$LIBDIR`, which should become `cygpath -m \$LIBDIR`.

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 […]