Using the formal definition of Event systems in Section 6.4 of the Shaw & Garlan text [SG96] (which reprints [GN91]), formally characterize a spreadsheet system as an event system. For the purposes of this assignment you can consider a spreadsheet to be an 1#1 matrix. Some of the entries in this matrix will have a VALUE. Some of the entries will also have an associated EQUATIONthat describes the value of that entry as a function over other entries in the spreadsheet. When spreadsheet entries are changed, the equations that depend on those entries are implicitly reevaluated. As with the blackboard, you need not formalize the run time mechanism of a spreadsheet.
You might find the following definitions to be a useful starting point:
2#2
3#3
In other words, we take VALUE and EQUATION to be primitive types, and a matrix position, Pos to be a pair of natural numbers. We assume (axiomatically) that we can determine for each equation what its parameters are and also how to evaluate it for actual values. (The invariant guarantees that the number of formal parameters must match the number of actual parameters.)
With this as a basis you can then define a spreadsheet along the following lines:
4#4
The symbol 5#5 indicates that each position is associated with a unique component.
You may assume that each Component in a spreadsheet (associated with a box via boxes) can update its value using the method Updatewhenever it gets the Reevaluate event. Your task is to add any appropriate additional state and the state invariants. In particular, the state invariant should explain how EM is determined by the other parts of the spreadsheet.
If you want to use Fuzz to check your specification, the source for this assignment and a copy of the Z description for the event system described in [GN91] is available in the class directory under /afs/cs/academic/class/15675/assignments/a4.