New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Syntax for Properties #711

Closed
DavePearce opened this Issue Mar 10, 2017 · 2 comments

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Mar 10, 2017

(follows on from #293 and #212)

There is a strong need for an abstraction mechanism for specifications / invariants. For example, consider this simple Whiley program:

function fill(int[] xs, int x, int n) -> (int[] rs)
requires 0 <= n && n < |xs|
// Size of result matches input array
ensures |xs| == |rs|
// All elements upto n now contain x
ensures all { k in 0..n | rs[k] == x }
// All other elemnts are unchanged
ensures all { k in n .. |xs| | rs[k] == xs[k] }:
    //
    nat i = 0
    int[] oxs = xs
    //
    while i < n
    // Size remains unchanged
    where |xs| == |oxs|
    // All elements seen so far filled with x
    where all { j in 0..i | xs[j] == x }
    // All unseen elements remain unchanged
    where all { j in 0..|xs| | xs[j] == oxs[j] }:
        xs[i] = x
        i = i + 1
    //
    return xs

In the example, several clauses in the post-condition and loop invariant are both repetitive, and also difficult to understand. This proposal is to provide an abstraction mechanism, called a property, which can improve this situation. The above example would be thus transformed:

property filled(int[] arr, int start, int end, int value):
    all { i in start ... end | arr[i] == value }

property unchanged(int[] before, int[] after, int start, int end):
    all { i in start .. end | before[i] == after[i] } 
    
function fill(int[] xs, int x, int n) -> (int[] rs)
requires 0 <= n && n < |xs|
// Size of result matches input array
ensures |xs| == |rs|
// Elements upto n contains x, others unchanged
ensures filled(rs, 0, n, x) && unchanged(xs,rs,n,|xs|):
    //
    nat i = 0
    int[] oxs = xs
    //
    while i < n
    // Size remains unchanged
    where |xs| == |oxs|
    // All elements seen so far filled with x, others unchanged
    where filled(xs, 0, i, x) && unchanged(oxs,xs,i,|xs|)::
        xs[i] = x
        i = i + 1
    //
    return xs

Properties are treated inherently differently from functions by the verifier. In particular, they are not regarded as uninterpreted functions. Instead, they are essentially inlined during the theorem proving process.

An important question is whether or not to support recursive properties. This would certainly seem beneficial for describing properties over recursive data structures. However, their treatment within the theorem prover of course will warrant some attention.

Finally, regarding the name property. In other languages (such as Dafny), the keyword used is predicate. I prefer property as it is somehow "less formal" sounding, and yet also provides some intuition that is helpful for understanding the distinction between functions and methods.

@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce Mar 10, 2017

Member

An interesting question is whether or not the syntax should be:

property filled(int[] arr, int start, int end, int value)
where all { i in start ... end | arr[i] == value }

The advantage of this approach is that, as for type invariants, we can spread them across multiple lines in a syntactically useful fashion.

Member

DavePearce commented Mar 10, 2017

An interesting question is whether or not the syntax should be:

property filled(int[] arr, int start, int end, int value)
where all { i in start ... end | arr[i] == value }

The advantage of this approach is that, as for type invariants, we can spread them across multiple lines in a syntactically useful fashion.

DavePearce added a commit that referenced this issue Mar 13, 2017

Add test cases for property syntax #711
This adds a bunch of test cases (which currently fail) that use the new
property syntax.  Actually, the use of properties in the test cases
looks very nice.

DavePearce added a commit that referenced this issue Mar 16, 2017

Add test cases for property syntax #711
This adds a bunch of test cases (which currently fail) that use the new
property syntax.  Actually, the use of properties in the test cases
looks very nice.

DavePearce added a commit that referenced this issue Mar 17, 2017

Add test cases for property syntax #711
This adds a bunch of test cases (which currently fail) that use the new
property syntax.  Actually, the use of properties in the test cases
looks very nice.

DavePearce added a commit that referenced this issue Mar 17, 2017

Support for parsing / interpreting properties #711
This adds support for parsing properties and interpreting them.  Work
remains to turn them into verification conditions.
@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce Mar 17, 2017

Member

Done!

Member

DavePearce commented Mar 17, 2017

Done!

@DavePearce DavePearce closed this Mar 17, 2017

DavePearce added a commit that referenced this issue Mar 19, 2017

Bug fix related to #711
Apparently, there were some aspects of properties which were not yet
implemented properly.  In particular, the binary format for reading /
writing properties was not correctly updated.  Likewise, the interpreter
was not looking up properties correctly either.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment