CS 8113g Spring 1995

Specification and analysis of interactive systems

CS 8113g Spring 1995

Lecture 9: More Reasoning

Date: April 25, 1995
Scribe: Scott McCrickard

Preview

Thu May 4 - Project Presentations (in Z)

Homework (as presented by Dierdre)

Dierdre has been specifying Mathematica using Z. Mathematica can be looked at as a collection of notebooks. Notebooks are broken into cells, which themselves can be broken into cells. At the lowest level, cells contain text, graphics and sound.

First, we need to identify primitive cells; that is, associate a content with a cell by defining a function. 

   Content ::= Text | Sound | Graphics

   [CELL]

   typecheck:Cell -> Content
How would one do that in LaTeX? 
   \begin{axdef}
   typecheck:Cell \fun Content
   \end{axdef}
What about more complex cells that could contain other cells? Just add another type to Content. 
   Content ::= Text | Sound | Graphics | Complex
Now we're going to define a notebook in which cells can have children. Note that the notebook has a tree-like parent-child relationship.

In the below description, P is a script P, @ separates declaration from predicate in universal quantification, V = forall, ! = not, {} = empty set. 

  __ Notebook _____
  |
  | children CELL -> P CELL
  | cells : P CELL
  |___
  |
  | cells = dom children
  | Vc : CELL | children(c) = {} @
  |       !(typecheck(c) = Complex)
  |
  | Vc : CELL | children(c) != {} @
  |       typecheck(c) = Complex
  |________________
The above description describes a connected graph, but it does not reflect the tree properties and other unique properties of the notebook. If desired, we could have defined it to reflect these properties, but we didn't.

Operations such as grouping, ungrouping, add/remove/modify cells are easy to define. Operations such as display and collapse are more difficult and will be discussed in detail on Thursday.

A Correction from Gregory

Last Thursday, Gregory started to define some properties of an editor and some confusion arose. Today he elaborated on his definitions. The full description of the proofs are in the notes for the last lecture.

Recall that we were discussing what can happen in our Editor when you do a move left (ML) followed by a move right (MR) as defined with respect to the primitives ML_0 and MR_0. Here are the four possibilities. 

   ML;MR = (ML_0 v AtBeg) ; (MR_0 v AtEnd)
         = (ML_0 ; MR_0) v (ML_0 ; AtEnd)
            v (AtBeg ; MR) v (AtBeg ; AtEnd)
Note that the second case cannot happen. If you move left, you won't be at the end. The third case is the unintuitive one.

Below we relate these properties to the Editor. 

   ML,MR |- !AtBeg => Chi Editor

Multiple Buffers in our Editor Example

In the Editor example, we only considered editors with a single buffer. Today we define a multi-buffer editor.

Some new notation was introduced today. Theta Editor refers to all components of Editor. It is a shorthand method for referring to all of the values of a given instance of a schema as one entity. In the below example, we can simply write buffers'(currentb) = Theta Editor rather than specifying the equation for each of the components of buffers(currentb) and Editor. Note that this makes the expression much shorter and easier to understand.

Below is the description of the multi-buffer editor. 


  __ MultiEditor _____
  |
  | buffers: BUFFID -|-> Editor
  | currentb : BUFFID
  |___
  |
  | ...
  |________________


  __ Frame
  |
  | Delta MultiEditor
  | Delta Editor
  |___
  |
  | currentb' = currentb
  | Vb : BUFFID | b != currentb o
  |      buffers'(b) = buffer(b)
  | buffers(currentb) = Theta Editor
  | buffers'(currentb) = Theta Editor'
  |________________
Note that current doesn't change except to change the current buffer.

In the next class we're going to discuss how to define displays. Don't be late!

Created May 18, 1995 16:16:28 by abowd@cc