• Special Pages
• User

Help

# Tutorial Modeling Infinite Datatypes

This tutorial describes how to model (and how not to model) infinite datatypes so that they can be animated with ProB. We illustrate this using a Stack datatype.

This does not work

```MACHINE StackAxioms1
SETS Stack
CONSTANTS pop, push,empty
PROPERTIES
empty:Stack &
pop : Stack \ {empty} --> Stack &
!s,x . (s : Stack & x : NAT => pop(push(s |-> x)) = s)
& push: Stack*NAT --> Stack \ {empty}
END
```

To do: explain why: infinite Stack would be required; ProB does not support infinite deferred sets. We need to do a more constructive definition and use the infinite set ProB knows about: INTEGER.

```MACHINE StackConstructive
/* A machine that shows how to model a stack of type RANGE so that it can
be animated and validated with ProB */
/* We could have used the sequence operations instead;
our intention was also to show how you can model this in Event-B */
DEFINITIONS Stack == (INTEGER <-> RANGE)
SETS RANGE
CONSTANTS empty, push, pop, tops
PROPERTIES
empty : Stack & empty = {} &
push : (RANGE * Stack) <-> Stack &
push = %(x,s).(x:RANGE & s:Stack | s \/ {card(s)+1|->x}) &
pop: Stack <-> Stack &
pop = %s.(s:Stack| {card(s)} <<| s) &
tops: Stack <-> RANGE &
tops = %s.(s:Stack| s(card(s)))
ASSERTIONS
/* the assertions cannot be checked by ProB, they will trigger
the expansion of the infinite functions above */
tops: Stack \ {empty} --> RANGE;
push: (RANGE*Stack) --> Stack \ {empty};
pop: Stack \ {empty} --> Stack
VARIABLES cur
INVARIANT
cur: Stack
& cur : seq(RANGE) /* a slightly stronger invariant */
INITIALISATION cur := empty
OPERATIONS
Push(yy) = PRE yy:RANGE THEN cur:= push(yy,cur) END;
Pop = PRE cur /= empty THEN cur := pop(cur) END;
t <-- Top = PRE cur /= empty THEN t := tops(cur) END
END
```

As the screenshot illustrates, this model can now be animated with ProB. Observe how the functions push, pop and tops are kept symbolic in the State View.