Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Syntax for Handling Multiple Returns #94

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

(follows on from #87)

At the moment, it is valid in WyAL to declare a function with multiple returns, such as:

function f(int x) -> (int y, int z)

However, at this stage, there is not syntax for extracting the individual elements of a function which has multiple returns. For example, suppose this Whiley:

   ...
   x,y = f(0)
   ...

Then we'd want to generate an expression of the form (x == f(0)#0) && (y == f(0)#1) where the # indicates the return selector. The key here is really that every function invocation in WyAL must refer to an individual return value. This is because there are no tuple values at this time.

Proposed Syntax

Options:

(x == f(0)#0) && (y == f(0)#1)
(x == f(0):0) && (y == f(0):1)
(x == f(0)'0) && (y == f(0)'1)

Amazingly, the latter does not look that bad!!

DavePearce commented 7 years ago

Sadly, in the end I went with the # syntax because the ' syntax was conflicting with single character literals.