File System Lesson V

Start Over . back . next

Now that we've built a model that ensures the structural correctness of our file system, we can begin to analyze operations that mutate file systems. Let's begin with a function to define the move operation. But first, a philosophical note...


In an imperative model, you might ask yourself "how can I make X happen?". In a declarative model (like Alloy), you ask yourself "how would I recognize that X has been accomplished?".

One reflection of this is that functions in Alloy only ever evaluate to true or false. In an imperative language, you might make the move function take a file system, an object to be moved, and a directory to move it to as arguments, and then have it return a new file system where that object has been moved to that directory. What we do in Alloy is to make all those things arguments to the function, including the 'output'. The function then returns true if the output parameter is valid given the input parameters, and false if it is not. If we later say "make sure this function is always true", then you will only get back examples where valid moves occur.

1. pred move [fs, fs': FileSystem, x: FSObject, d: Dir] {
2.     (x + d) in fs.live
3.     fs'.parent = fs.parent - x->(x.(fs.parent)) + x->d
4. }

The predicate move is true if file system fs' is the result of moving file system object x to directory d in file system fs. In this function, we can think of file system fs as the pre-state and fs' as the post-state, but the prime character has no semantic meaning in and of itself. Although it would be confusing, we could have named the pre-state fs' and the post-state fs.

Line 2 stipulates that the object to be moved and the destination directory of the move must both exist in the pre-state file system. Line 3 is a little tricky. It states that the parent relation in the post state is the same as the pre state, except that the mapping from x to x's old parent is replaced by the mapping from x to x's new parent d.


We can view an example of a move by adding the following command to our model and then executing it.

  run move for 2 FileSystem, 4 FSObject

Now let's add an assertion to give us confidence that the move is correct. The following check claims that the move operation does not alter the set of objects in the file system.

  moveOkay: check {
    all fs, fs': FileSystem, x: FSObject, d:Dir |
      move[fs, fs', x, d] => fs'.live = fs.live
  } for 5

The above syntax combines the definition of an assertion with the scope you intend to search for. And it's equivalent to the following longer form:

  assert moveOkay {
    all fs, fs': FileSystem, x: FSObject, d:Dir |
      move[fs, fs', x, d] => fs'.live = fs.live
  }

  check moveOkay for 5

If you go to the Executes menu item in the menu bar, and select moveOkay, Alloy Analyzer will report that there is no counterexample to this assertion within a scope of 5.


Our move predicate seems to work fine, so let's move on to writing a remove predicate. In fact, we will write two remove predicates: one to remove a single file or empty directory, and one to perform recursive removal:

1. pred remove [fs, fs': FileSystem, x: FSObject] {
2.   x in (fs.live - fs.root)
3.   fs'.parent = fs.parent - x->(x.(fs.parent))
4. }

1. pred removeAll [fs, fs': FileSystem, x: FSObject] {
2.   x in (fs.live - fs.root)
3.   let subtree = x.*(fs.contents) |
4.      fs'.parent = fs.parent - subtree->(subtree.(fs.parent))
5. }

Line 2 is the same in remove and removeAll. It stipulates that the file system object to be deleted, x, must be in the pre-state file system, fs, but that it cannot be the root of fs. Certainly, it doesn't make sense to delete a file from a file system if it isn't there; nor does it make sense to delete the root of a file system (since we require all file systems to have roots).

Line 3 of remove constrains the post-state file system to be the same as the pre-state file system, except with the mapping from x to x's parent removed.

Line 3 of removeAll uses a let statement. A let statement acts as a macro replacing the right-side of the assignment wherever the left-side of the assignment appears. That is, lines 3 and 4 desugar to (and are interpreted by Alloy as) the following:

  fs'.parent = fs.parent - (x.*(fs.contents)) -> (x.*(fs.contents)).(fs.parent)

Because it is just syntactic sugar, the let construct is never necessary, but it can make Alloy model more understandable.

The expression on the right hand side of the assignment, x.*(fs.contents), is the set of files and directories obtained by following the contents relation in file system fs zero or more times starting at file system object x. In other words, it is the set of all file system objects in the subtree rooted at x. Thus, this constraint states that the parent relation in the post-state file system is the parent relation in the pre-state minus all mappings from objects in the subtree to their parents.


Now let's verify the correctness of our remove functions with assertions. Our assertions claim that the functions to do not alter the root of the file system; that the rows in the contents relation of the post-state is a subset of the rows in the pre-state; and that they remove exactly the objects they should.

  removeOkay: check {
    all fs, fs': FileSystem, x: FSObject  |
      remove[fs, fs', x] => fs'.live = fs.live - x
  } for 5

and

  removeAllOkay: check {
    all fs, fs': FileSystem, d: Dir |
      removeAll[fs, fs', d] => fs'.live = fs.live - d.*(fs.contents)
  } for 5

Alloy produces a counterexample for each of these commands; so the assertions must not be true. But before we even begin to inspect the counterexamples, let's first lower the scope of the check commands to 4, recompile, and execute the commands again. Again, alloy produces counterexamples. Then we try a scope of 3, then 2, and finally 1. It turns out the smallest scope in which a counterexample still exists is 2. It is typically helpful to progressively lower the scope on the check commands until no more counterexamples are found.

We will examine and correct these errors in the next lesson.


Start Over . back . next