Articles

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!

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

    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:

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

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

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>