Executing Specifications Using Synthesis and Constraint Solving - Runtime Verification - page 5

3 Language
We next present a simple functional language that we use to explore the ability
to do verification as well as to execute and compile constraints.
3.1 Implementation Language
As the implementation language we consider a Turing-complete Scala fragment.
For the purpose of this paper we assume that programs consist of a set of side-
effect-free deterministic mutually recursive functions that manipulate countable
data types including integers, n-tuples, algebraic data types, finite sets, and
finite maps. We focus on functional code. Our implementation does support
localized imperative features; for more details see [9]. We assume that recursive
functions are terminating when their specified preconditions are met; our tool
applies several techniques to establish termination of recursive functions.
3.2 Function Contracts
Following Scala's contract notation [51], we specify functions in the implemen-
tation language using preconditions ( require ) and postconditions ( ensuring ). The
declaration
def f(x:A) : B = {
body
} ensuring ((res:B) ⇒ post(res))
indicates that the result computed by f should satisfy the specification post .Here
res ⇒ post(res) is a lambda expression in which res is a bound variable; the ensuring
operator binds res to the result of evaluating body . The expression post is itself
a general expression in the implementation language, and can invoke recursive
functions itself.
3.3 Key Concept: Constraints
Constraints are lambda expressions returning a Boolean value, precisely of the
kind used after ensuring clauses. To express that a constraint should be solved
for a given value, we introduce the construct choose . The expression
choose((res:B) ⇒ C(res))
should evaluate to a value of type B that satisfies the constraint C . For example,
an implicit way to indicate that we expect that the value y is even and to compute
y/2 is the following:
choose((res:Int) ⇒ res + res == y)
The above expression evaluates to y/2 whenever y is even. Note that C typically
contains, in addition to the variable res , variables denoting other values in scope
(in the above, example, the variable y ). We call such variables parameters of the
constraint.