-
Notifications
You must be signed in to change notification settings - Fork 20
Keyword Dictionary
Indicates a total function. The base form for a function type. It does not permit the functions to have requires or reads clauses as part of the function definition.
Indicates a partial function. This is similar to a total function but allows requires clauses as part of the function definition.
The elephant operator. This is used as a short-circuiting exception/error/option operator. It indicates that the left side will have a value upon completion or the operator will return from the current scope with an exception/error/failure state. This can be used with multiple returns as well. This operator will work as intended when the first of the multiple returns is a supporting type.
In practice, this can be used much like an exception.
method GetInt() returns (ret: Result<int, string>) {
// ...
}
method GetNumbers() returns (ret: Result<int, string>, y: float, z: string) {
// ...
}
method Caller() returns (result: Result<bool, string>) {
var intValue :- GetInt();
var intValue, floatValue, stringValue :- GetNumbers();
return Success(intValue == floatValue);
}Used in several contexts to separate bound variables from the body of the definition.
Opaque is an attribute that can be attached to a function to indicate to the verifier to not try and peek inside, but rather take its specification at face value.
? is as a quasi-optional indicator:
- For datatypes, it can be used to determine if the datatype is a specific value type.
- For classes and traits, it means the type can be the class/trait or
null.
datatype AorB = A | B
var example := A;
assert example.A?;
class C {}
var cls1: C := new C();
var cls2: C? := null;Indicates an any function. This is similar to the total and partial functions but allows both requires and reads clauses as part of the function definition.
Creates a new datatype. It is used to create enums and record/struct types and cannot be null.
datatype NumberRecord = NumberRecord(intField: int, strField: string)
var threeRecord := NumberRecord(3, "three");forall evaluates an expression for each value provided.
Defines a mapping (ie hashmap, dictionary, etc).
Defines a set.