modelling state

for each procedure

sig State { type { Object } state { … } }

for each class C

state { C : Object }

for each arg or var v of class C

state { v : C ? }

for each field f in class C of class D

state { f : C -> D ? }

example
class List {List next}

void insert (List first, List rest) { first.next = rest }

translation
sig insertState { type {Object}

state {first, rest : List ? , next : List -> List ? } op insert () { first.next’ = rest all x | x != first -> x.next = x.next’
rest’ = rest } }

Previous slide

Next slide

Back to first slide

View graphic version