// module declaration
module qualified/name
// imports
open other_module
open qual/name[Param] as Alias
// paragraphs (any order)
sig name ...
fact name { formulas }
pred name { formulas }
assert name { formulas }
fun name [Param] : bounding-expr {
body-expression
}
run pred-name for scope
check assertion for scope
sig qualified-name ... {
field declarations
}
// or ...
sig qualified-name ... {
field declarations
}{
signature facts
}
sig S { ... } { F },
F is interpreted as if the model read
sig S { ... } fact { all this : S | F′ },
where F′ is like F but each
name f is expanded to this.f
if f names a field of S. Write @f
to suppress the expansion.
sig qname { ... }
sig qname extends superclass { ... }
sig qname in sup { ... }
sig qname in sup1 + sup2 + ... { ... }
sig qname1, qname2, ... { ... }sig qname1 { ...} sig qname2 { ... } ...
one sig qname { ... }
lone sig qname { ... }
some sig qname { ... }
fact name { formulas }
fact { formulas } // name optionalpred name { formulas }
pred name [decl, decl2 ...]{ formulas }run to request an instance satisfying the predicate:run name
run name for 2 run name for 2 but 1 sig1, 5 sig2
assert name { formulas }check to look for counter-examples:check name for 2 but 1 sig1, 5 sig2
fun name [decl, ...] : e1 { e2 }name : bounding-expressionname1, name2 : bounding-expression // or disj name1, name2 : bounding-expression
disj can also be on the right:sig S {f : disj e}all a, b : S | a != b implies no a.f & b.f
≡ all disj a, b : S | disj [a.f, b.f]
name1 : bounding-expression // equivalent to: name1 : one bounding-expression
name2 : lone expr // at most one name3 : some expr // one or more name4 : set expr // zero or more
r : e1 -> e2
r : e1 -> one e2 // total function r : e1 -> lone e2 // partial function r : e1 one -> one e2 // 1:1 (bijection)
set1 in set2 set1 = set2 scalar = value
some relation-name no r1 & r2 // etc.
some var : bounding-expr | expr all var : bounding-expr | expr one var : bounding-expr | expr lone var : bounding-expr | expr no var : bounding-expr | exprTrue iff expr is true for some, all, exactly one, at most one, or no elements of the set denoted by bounding-expr
not,
and,
or,
implies,
iff) can form compound booleans;
most of them apply only to
boolean expressions.boolean and boolean2 not boolean or boolean2 boolean implies boolean2 // etc.
boolean implies expression boolean implies expr1 else expr2
let decl, decl2 ... | expression
let decl, decl2 ... { formulas }@ + simple name,
or this.none (the empty set),
univ (the universal set),
iden (the identity function).~,
*,
^) and r is binary..,
&,
+,
-,
<:,
:>,
++) and a, b are n-ary relations.set] -> [mult|set] r2.plus,
minus,
mul,
div,
rem) apply only to
integer expressions. They name
ternary relations, so x + 1
can be written as any of:
plus[x][1],
plus[x,1],
x.plus[1], or
1.(x.plus).
disj[ A, B, ... ] (true iff
all arguments are pairwise disjoint)sum[ set of Int ] (returns
sum of argument)univ (universal set),
none (empty set),
iden (identity relation).
~r (transpose / inverse),
^r (positive transitive closure),
*r (reflexive transitive closure)
a.b
b[a] (also for function application, f[t]).
N.B. dot binds tighter than box, so
a.b[c] ≡ (a.b)[c]
s <: a (domain restriction),
a :> s (range restriction)
a -> b (Cartesian product)
a & b (intersection†)
r1 ++ r2 (relational override)
#a (how many members in a?‡)
a + b (union†),
a - b (difference†)
no,
some,
lone,
one,
set
not,
!
in,
=,
<,
>,
=,
=<,
=>
not,
!
and,
&&
implies,
else,
=>
iff,
<=>
or,
||
let,
no,
some,
lone,
one,
sum
a and b must have matching arityp => q => r
≡
p => (q => r)
else binds to the
nearest possible implies:
p => q => r else s
≡
p => (q => r else s)
a.b.c
≡
(a.b).c
\ ` $ % ?
=> >= =< -> <: :> ++ || // -- /* */ are single tokens
(so: != can be written ! =)// to end of line;
from -- to end of line;
/* to next */ (no nesting).
this (e.g. xyz, this/a/b/c, util/ordering)abstract
all
and
as
assert
but
check
disj
else
exactly
extends
fact
for
fun
iden
iff
implies
in
Int
let
lone
module
no
none
not
one
open
or
pred
run
set
sig
some
sum
univ