Datatype Rules
From Event-B
Revision as of 10:22, 6 September 2010 by imported>Nicolas (New page: Datatype rules may seem a bit difficult to understand at first sight. Here are a few examples intended to make them clearer. They applied to the following datatypes: Directions: direct...)
Datatype rules may seem a bit difficult to understand at first sight. Here are a few examples intended to make them clearer.
They applied to the following datatypes:
Directions:
direction ::= north | east | south | west
Let denote a function
first two arguments are a start position, third is a direction, result is the end position.
Lists:
list(α) ::= nil | cons( head : α, tail : list(α) )
Let denote a predicate
meaning that the first argument is a member of the list.
Trees:
tree(α) ::= empty | node( left : tree(α), value : α, right : tree(α) )
Let denote a function
\operatorname{height}(Tree) \tfun \N defining the height of a tree
Contents
Distinct Case
The rule states
Application to directions
TODO
!x,y,dir . move(x,y,dir) /= x |-> y
Application to lists
TODO
!l oftype list(\Z). #x. member(x,l) & (!y. member(y,l) => y <= x)
evidence that nil list has been forgotten in the predicate
Application to trees
TODO
Induction
TODO