Index

A

Alloy

assert, [1], [2] atoms

B

Boolean operator see logical operator

C

command check, [1], [2], [3], [4] run, [1], [2], [3] constant iden none, [1] univ

converse see transpose

D

distributed protocol leader election

dot join see composition

E

enum keyword see enumeration signatures evaluator event effect, [1] enabled frame condition, [1] guard, [1]

F

fact fairness strong weak fields field declaration, [1] variable fields

first-order logic fun keyword see function, Alloy function, Alloy, [1] function, logic

I

instance, [1], [2] exploration, [1], [2] snapshot

invariant

L

liveness logical operator conjunction, [1] disjunction, [1] else, [1] equivalence, [1] implication, [1] negation, [1]

M

model checking bounded, [1] unbounded, [1] model, Alloy see specification model, logic see instance module ordering parameterised predefined

multiplicity constraint lone keyword one keyword, [1] set keyword some keyword

P

pred keyword see predicate, Alloy predicate

predicate, Alloy predicate, logic, [1] proposition propositional logic

Q

quantifier disj, [1], [2] existential, [1] higher-order universal, [1]

R

relation abstraction arity, [1] bijection binary, [1] entire function injection injective representation simple surjection surjective ternary, [1]

relation comprehension, [1] relational logic, [1] relational operator box join Cartesian product, [1] composition, [1] difference, [1] domain restriction, [1] intersection, [1] override range restriction, [1] reflexive transitive closure, [1] transitive closure, [1] transpose union, [1]

S

safety scenario scopes, [1] exact scopes setting scopes, [1] steps, [1] sig keyword see signature declaration signature abstract enumeration signatures, [1] extension vs inclusion signature declaration, [1] subset signatures top-level signatures variable signatures

Skolemization solver, [1] specification stuttering symmetry breaking, [1]

T

temporal operator after, [1] always, [1], [2] eventually, [1] historically, [1] once sequence themes customisation, [1], [2], [3] magic layout

total order transition system type system arity error type-system irrelevance error

V

var keyword variable fields variable signatures