Languages like Eiffel
or Spec# incorporate a
methodology called Design by Contract
to reason about programs, libraries, methods. It allows to write more
secure and correct software and specify its behavior.
Languages following this design must support writing explicit requirements
about values on which a program operates, including:
- preconditions - some fact (boolean condition) that must be satisfied in order to call a method; mostly concerning passed parameters, but can be used to enforce any condition computable at method invocation begining
- postconditions - a fact that must be satisfied after calling a method, for example about the return value
- invariants - a property of a program, which does not change in time (like a non-decreasing order of elements in list, etc.)
- other restrictions in behavior of some part of a program (like, for example, the fact that a method does not change the state of a class)
We are currently on the way to add an ability to define most of those features
to Nemerle. In the following subsections we present their current state, design
and plans for the future.
Preconditions of a method (conditions that need to be satisfied
before the method is called) can be specified using the
Requires
attribute.
class String
{
public Substring (startIdx : int) : string
requires startIdx >= 0 && startIdx <= this.Length
{ ... }
}
Using this attribute we can add an arbitrary assertion, keeping the
body of the method clean and verbose. The compiler automatically adds
runtime checks at the beginning of the method. If the condition is
violated, then an
AssertionException
is being thrown with
an appropriate message containing this expression.
Requires
and other attributes can occur many times before a single
method. They can be also defined directly on parameters.
ConnectTrees (requires (!tree1.Cyclic ()) tree1 : Graph,
requires (!tree2.Cyclic ()) tree2 : Graph,
e : Edge) : Graph
{ ... }
Following the same design, we can define postconditions which the
method must satisfy. This is an assertion that must be true
after the execution of the method. If the method returns a value, then a
symbol
value
is available inside the expression
stating an assertion.
class LinkedList
{
public Clear () : void
ensures this.IsEmpty
{ ... }
public Length () : int
ensures value >= 0
{ ... }
}
An even more powerful feature is to give a condition, which
must be true all the time during the execution of a program.
We can attach invariant to any class by writing
Invariant
attribute before its definition.
class Vector [T]
invariant position >= 0 && position <= arr.Length
{
private mutable position : int = 0;
private arr : array [T] = array [];
public push_back (x : T) : void
{ ... }
This way we can ensure that the state of our object is valid according to
defined rule.
This naturally brings the problem with changing variables,
which are dependent on each other in invariant. Suppose we have
an assertion x == y + 5
and we cannot change any of the variables.
Thus, we need a mechanism for making transactions, within which
invariants are temporarily turned off.
We follow the design of Spec# and add a special construct to expose
the object to changes.
expose (this) {
x += 3;
y += 3;
}
expose
takes reference to the object to be exposed and
executes the given code.
In the matter of fact, invariants are not checked all the time during
execution. It would be too expensive to validate them at any assignment
or call to external function. We again follow design of Spec# and
run assertions at the end of expose
blocks and after execution
of all public methods.
There are few more things which we want to implement in more or
less distant future:
- Make these attributes inherited in classes deriving from ones decorated with assertions. For example, we define an interface with preconditions and postconditions and we can be sure, that every class implementing this interface will comply to them.
- Plug a theorem prover designed for Spec# into Nemerle, so we can check assertions not only in the runtime, but also statically at compile-time.
- Invariant attribute needs much work to follow all functionality of its Spec# counterpart.