Formal Software Design with Alloy 6
Contents
An overview of Alloy
Structural design with Alloy
Protocol design with Alloy
Alloy modelling tips
Teaching with Alloy4Fun
A relational logic primer
A temporal logic primer
Acknowledgements
Bibliography
Index
Formal Software Design with Alloy 6
»
Index
Index
A
|
B
|
C
|
D
|
E
|
F
|
I
|
L
|
M
|
P
|
Q
|
R
|
S
|
T
|
V
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