Formally characterize a spreadsheet system as an event system. For
the purposes of this assignment you can consider a spreadsheet to be
an 
matrix. Some of the entries in this matrix will have a
VALUE. Some of the entries will also have an associated EQUATION
that 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:
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:
The symbol 
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 Update whenever 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.