File System Lesson IV

In this lesson, we do not add any new features to the model, but instead we rewrite part of it to show you a different way to doing things. The resulting model is semantically equivalent, but is a bit more concise and arguably clearer.

Two of the four constraints which were in the FileSystem appended fact have been removed:

  no root.parent
  contents in live->live

These constraints have been built into the other ones. First of all, the line which used to read

  root: Dir,

now reads

  root: Dir & live,

This defines the root of a FileSystem to be in the set of live objects of its FileSystem, and not just be any old directory. (since it is in the intersection of Dir and live).

Secondly, the lines which use to read

  parent: FSObject ->lone Dir,
  contents: Dir lone-> FSObject

now read

  parent: (live - root) ->one (Dir & live),
  contents: Dir -> FSObject

This is the same trick, but a little bit messier because it has been done to higher arity relations (relations with more than 2 entries in each row). The parent relation maps every live object (except the root) to exactly one live Dir. The contents relation can be relaxed to just say it maps from Dir to FSObject (since later we have "contents = ~parent" so the contents relation will be exactly correct, and we don't need to write "Dir lone->FSObject" here).

Also notice that the lone multiplicity markings have been replaced by one's. Where a lone indicated "0 or 1", a one indicates "exactly 1". Thus the first line makes sure that each live non-root object has exactly one parent.

In the next lesson, we add dynamic operations to the model, move and remove.