Articles

Illustrating Compile-Time Verification in Whiley

With the latest release of Whiley, compile-time checking of constraints can be enabled with a command-line switch.  So, I thought a few examples of this were in order.

Example: Absolute of an Integer

Consider this simple program:

define nat as int where $ >= 0

nat abs(int x):
    return x

This defines a type nat which is an int whose values are non-negative.  The function abs(int) accepts an int and returns a nat.  However, it contains a bug because int does not subtype nat (since int includes negatives whilst nat does not).  We can compile this on the command-line like so:

% wyjc -X verification:enable=true example.whiley
./example.whiley:4: constraint not satisfied
    return x
    ^^^^^^^^

The command-line switch -X verification:enable=true turns on compile-time verification. This is not enabled by default because it is experimental. As we can see, the compiler has correctly spotted the error on line 4. We can fix the code like so:

define nat as int where $ >= 0

nat abs(int x):
    if x >= 0
        return x
    else:
        return -x

This will now compile correctly with verification enabled.  As you can see the verifier is able to correctly reason about the effect of conditional statements.

Example: Maximum of two Integers

As another illustration, consider the following (broken) implementation of the max(int,int) function:

int max(int x, int y):
    if x < y:
        return x
    else:
        return y

At this point, the function does the opposite of what you would expect (i.e. it computes the minimum of x and y because of a bug). However, the function will compile with verification enabled because the code meets the given specification. Let us improve the specification a little by introducing some constraints:

int max(int x, int y) ensures $ == x || $ == y:
    if x < y:
        return x
    else:
        return y

The given constraint states the return value $ is equal to either x or y. However, this constraint is not strong enough to enforce that the maximum of x and y is returned. Hence, the code still compiles even with verification enabled. Finally, we add the missing bit:

int max(int x, int y) ensures ($ == x || $ == y) && x <= $ && y <= $:
    if x < y:
        return x
    else:
        return y

Compiling the above with verification enabled now gives the following error:

% bin/wyjc -X verification:enable=true max.whiley
./max.whiley:3: postcondition not satisfied
        return x
        ^^^^^^^^

At this point, we can fix the bug by changing the condition to be if x > y and it will compile correctly with verification enabled.

4 comments to Illustrating Compile-Time Verification in Whiley

  • This is very impressive and the most interesting part of Whiley IMO. I remember seeing it in action when you showed me your “new project” a couple of years ago. It’s good to see it making a resurgence. It seems reasonably straightforward how the compiler checks the constraint in this particular case, but I think there’s a place for future posts spelling it out a bit more! Whiley provides nice demonstrations of proofs in action in a simple practical language.

  • Hey Edmund,

    Yeah, it’s definitely the most interesting part of the language! And, also, the most tricky to get right. At the moment, it’s sketchy and has quite a few problems. Over the coming months, I’m planning to really get sorted. I definitely need to write more posts specifically about this, and how it all works in Whiley. Ah, so much to do!

  • Having a complete constraint does make the function seem a bit redundant! Have you had any thoughts about leaving the code out, and generating it from constraints? For instance, the constraint on max looks a lot like the Prolog code:

    max(+X, +Y, M) :-
    (M = X; M = Y),
    X =< M,
    Y =< M.

    I can mentally execute that in my head (using backtracking), but I must admit I’m having difficulty seeing how to translate it into the body of your function. Something needs to be translated into an if-statement but it’s hard to see what.

    Anyway, this is an idle thought and I’m not serious about Whiley generating code out of thin air from nothing but a constraint.

  • Hey Edmund,

    Have you had any thoughts about leaving the code out, and generating it from constraints?

    So, this is often referred to as program synthesis. This is an interesting area and it would be really cool to explore Whiley in this context. However, I consider it to be (far) future work as I really have my hands full already making Whiley work. It’s the kind of thing an interested student could take on as an MSc or PhD topic …

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>