Improved Property Syntax

[DavePearce]

Currently, the syntax for properties is pretty awful. Here's an example from the standard library:

// Check if two arrays equal for a given subrange
public property equals<T>(T[] lhs, T[] rhs, int start, int end)
// Arrays must be big enough to hold subrange
where |lhs| >= end && |rhs| >= end
// All items in subrange match
where all { i in start..end | lhs[i] == rhs[i] }

The essential point of properties (as it stands) are that they receive special status within the theorem prover. Specifically, properties can be inlined during the verification process. This provides significant additional expressivity over functions which are treated as uninterpreted during verification. In some sense, properties are like macros. Key points arising:

• Properties vs Functions. What is the essential difference here? One difference is that a function can hide its implementation (and, hence, change it at a later date). There are examples within the standard library (e.g. in std::array) with vaguely non-trivial implementations.
• Expression Syntax. The most obvious way to improve the syntax of properties is to allow an expression body. Combined with e.g. conditional expressions or general terms (Term Language? #80), this makes them quite powerful. A key arises around what restrictions (if any) should be placed on properties. Currently, properties can be recursive but, obviously, cannot contain loops. Should we allow them to contain loops?
• Specification Elements. Currently, properties cannot have pre-conditions or post-conditions. Does this still make sense?

Example 1

property sum(int[] arr, int i) -> int:
    if i >= |arr|:
        0
    else:
        arr[i] + sum(arr,i+1)

Example 2

type Link is { int data, LinkedList next }
type LinkedList is null | &Link

property disjoint(LinkstList l1, LinkedList l2):
    if l1 is null || l2 is null:
       true
    else:
       l1 != l2 && disjoint(l1->next, l2)

This is an interesting example as I'm trying to use a property in an impure fashion.