Constraints

Constraints list properties of instances without otherwise defining concrete forms of slots. Any class may include any combination of constraints and concrete definitions for any slot. A class describing constraints but leaving one or more slots otherwise undefined is termed abstract. Abstract classes are not instantiable.

ODL constraints are partial descriptions. Objects obey declarative constraints, but any behavior that is not ruled out is possible. The forms of constraints are limited to those that may be evaluated via combinations of static symbolic analysis, translator assisted instrumentation, and dynamic checks. Moreover, translators are only required to perform a subset of these measures, as described below. ODL does not specify whether or how conformance to others is enforced. ODL rules represent a compromise between expressive power and the inferential and run-time requirements upon implementations. Reification of specification constructs renders ODL at best incomplete as a declarative language. However, common constraints remain simply expressible and checkable.

Bindings

In ODL, the bindings from names to all slots except stored functions are fixed and common to all instances of a class. (This restriction may be lifted in a future version.) Bindings for stored slots may be changed during execution (via :=) unless they have been qualified as fixed. The binding for a slot qualified as fixed remains constant across the lifetime of each instance. The qualifier fixed may also be applied to a non-stored function to indicate that its value does not vary over time. (Note in this case that fixed refers to the value, not the binding.) The keyword own is an abbreviation for local fixed unique.

Types

All arguments and results (including function values) for all slots must be constrained by type, and optionally by qualifiers unique, common, and opt. Annotations for link types are partial specifications -- they list a type for the link, not necessarily the maximal (most exact) type.

In ODL, a message may be sent only if the recipient will eventually accept it. Determining conformance with this rule is in general undecidable. However, ODL programs must obey the weaker rule that a message be listed in a concrete definition only if it is provable that the recipient does not forever pend the message; i.e., if the message triggers a corresponding operation in at least one condition in a class declaration. The proof method is conservative, and based on type checking. In ODL every link is qualified with a type annotation indicating a class to which the referenced object must belong. The ODL type checker treats any attempt to send a message not listed in the indicated class (or superclass) as ``not provable'', thus as a programming error. However, the checker also admits invocations nested within conditionals checking (via `` in'') that the recipient is of a class supporting an operation. For example:

class A op m ... end end;
op calla(a: Any) { if a in A then a.m end; }

Function Value Constraints

Additional constraints may be declared via:

• Invariant ( inv) expressions that hold whenever objects are not engaged in operations (i.e., at all quiescent states).
• Short forms of equality invariants for functional slots: fn f ... = exp.
• Initial condition ( init) expressions holding upon construction.
• Short forms of equality-based initial conditions: fn f ... init= exp.

All constraints and conditions must be expressed within the (executable) value expression sublanguage of ODL. Invariants and initial conditions are boolean-valued expressions constructed from:

• Literals of value types.
• Equality operators ( =, ~=) on values of all types.
• Relational ordering operators ( <, <=, >, >= ) on values of int, char, real, time types. (ASCII compatible ordering is required of char.)
• Operators defined on boolean values: /\ ( and), \/ ( or), ~ ( not), => ( implies), and comma ( ,) (low precedence and). And and or are ``short circuiting'': successive terms of expressions need not be well-defined if the truth value is determined by previous terms.
• Operators defined on integer values ( +, -, *, div, mod).
• Operators defined on real values ( +, -, *, /).
• Real-valued mixed mode operators between integers and reals ( +, -, *, /).
• Operators defined on time values ( +, -), plus mixed mode *, div operations with integers.
• if exp then exp ... else exp end.
• Operator null( link ), defined on link types.
• Operator link in class, that is true if the object referenced by link is an instance of class or a subclass thereof.
• Field and subscript selection on records and arrays.
• Invocations of functional operations.

This sublanguage may be viewed as a very small pure functional language. ODL restricts the forms of functional operations in order to enable their use in declarative constraints. They thus play a dual role. From a computational perspective, they are restricted forms of operations, but from a declarative perspective they serve as symbolically tractable functions. The requirement that functional expressions be translatable into particular executable forms limits power and restricts expression. For example, bounded universal quantification is expressed via type annotations for function arguments.

In fact, inv and init are treated by translators as special declaration forms of ordinary functional slots. All inv constraints for a class are collected (clausally conjoined in listed order) in executable form as callable fn inv: bool that may be invoked at run-time. Similarly for fn init: bool. ODL does not otherwise require translators to perform symbolic analysis on constraints (e.g., to determine whether they are even satisfiable). Design checkers that perform such analyses may be constructed, but these capabilities are not demanded of translators.

Operation Constraints

Guards.

Guards are ``active'' preconditions listing the conditions under which nonfunctional, nonlocal operations may be executed. (``Passive'' preconditions describing alternatives within accepted operations are listed instead as ifs within effect expressions.) There are both ``outer'' and ``inner'' guards, of the form:

class C ...
 when c1 then
   op m1
     when m1c1 ==> ...
     elsewhen m1c2 ==> ...
     else ...  end
   op m2 ...
 elsewhen c2 then
   op m1 ...
 else ...  end
end

Any combination of ``outer'' clauses with embedded operations, and ``inner'' guards nested within operations are permitted. Stylistically, outer guards refer to object state, while inner forms refer to properties of message arguments of ops. Nested sets of guards are also permitted. Different versions of the same op may be declared in different arms of outer guards (as seen above for m1. Consistency rules for multiple versions are described in section 4.

Boolean expressions within when clauses are constructed using the above expression sublanguage. Translators must provide interference-free translation of guard expressions into executable form.

Like elsifs in most languages, the condition in each elsewhen clause is interpreted to include the negation of all preceeding conditions. This guarantees mutual exclusion of conditions. For example, elsewhen c2 above is interpreted as when ~c1 /\ c2.

Pending.

Pend is a pseudo-effect indicating that a message does not trigger an operation at all under the listed condition. If any other condition ever becomes true, the corresponding operation will be triggered accordingly. All explicit guards and non- local operations are considered to be encased within:

class ...
 when ready 
   ... 
 else 
   pend
 end
end

Ready is true when an object is not otherwise engaged in an operation. (This function does not actually exist and cannot be expressed in ODL.)

By default, if an op is listed in only one outer when then it it assumed to pend in all others in which it is not listed. Completely unlisted messages pend forever. Functional operations may pend only when an object is busy in another operation. Local operations are not processed as messages and cannot pend. Thus, no explict guards may be associated with functional and local operations.

Translators may employ any non-interfering mechanism to implement pend. The use of guards does not require that translators establish identifiable per-object message queues. No ODL constructs refer to queues. No run-time support is needed if a translator can determine that no pend conditions can ever be encountered for an object. When any of several messages may be accepted (i.e., clear guard conditions), any one of them may be chosen. Implementations may provide stronger ordering guarantees. Implementation limits in the number of possible simultaneously pending messages are permitted.

Translators cannot always statically detect situations in which conditionally accepted messages forever pend. They may provide run-time mechanisms to assist users in dealing with resulting deadlocks and overflows.

Effects.

Effects ( ==>) list conditions that must hold as a result of particular operations. Clauses within effect descriptions are defined using the constraint sublanguage extended with constructs:

exp'

The value of an expression as evaluated upon completion of the operation. (Unprimed forms within effects refer to evaluation upon commencement of operations.)

msg'

Assertion that the effects of msg hold at completion of the operation.

msg''

Assertion that the effects of msg hold (perhaps only briefly) at some point after commencement of the operation.

@boolexp

The time after which the operation commences at which the expression becomes true.

No translation into executable form is specified for effect expressions. In particular, effect expressions with double-primes cannot be translated in any useful manner since the time at which they should hold true is unbounded. However, static analysis tools may be constructed to determine satisfiablity of effect expressions and partial conformance of concrete forms. Other tools may be devised to help instrument checks for certain effects and/or to help generate test code.

ODL effects are not subject to ``frame assumptions'' that claim that properties that are not mentioned do not change. Any behavior consistent with constraints is allowed. All properties that must be preserved within ops should be explicit unless they are also listed in invs (which serve as implicit pre- and postconditions for all operations). In contrast, functional operations do obey frame axioms since they are computed in a side-effect-free manner.