This simple tutorial will help you with the first steps in Dynamite. It will guide you in opening the system for first time and closing your first proof. Please send any comments and/or problems to mmoscato@dc.uba.ar.
First download the Alloy specification we will use in order to explain the basic DPS commands. (This Alloy specification is based on the model example "file_system.als" that can be found in the Alloy Analyzer distribution.)
Then you may want to create a working directory, in which the Alloy specification must be placed. Once in that directory, to run the tool you only have to execute the shell script dps, that can be found in the root of the instalation. For example, if the Dynamite Proving System was installed in the directory /opt/dps you may run the script by typing
To load the Alloy specification, it is necessary to invoke the DPS command open-alloy-file. To do this, as usual in Emacs systems, you must hold the meta key (generally mapped to the Alt key) and press the x key, then you must type the name of the command: open-alloy-file. This kind of invocations will be abbreviated as
Then, the system will ask for the name of the Alloy file to be loaded. The specification will be shown in the current Emacs buffer.
To initiate the proof of an assertion, you must invoke the command
because this is the name of the assertion we will prove.
A message will appear indicating whether the underlying theories needed to prove the assertion could be correctly generated. If an error occurs during that process, it will be reported in the Emacs buffer called DynamiteTranslator output. To switch to this buffer, you may press the x key while holding the Ctrl key, then press the b key and after that enter the name of the buffer
After this, the main goal will be displayed in the *pvs* buffer. In this case, you will see the following
As in PVS, the user commands are typed in the Rule? prompt. The first command we will introduce, will be (skosimp*) to skolemize the quantified variables.
The quantified variables have been replaced by fresh new constants. Now, we want to introduce the case in which oh_1 is the root directory. To do that, we will use the command dps-case. This command application yields two subgoals: NoDirAliases.1 and NoDirAliases.2. The former has the Alloy formula oh_1 in Root as a new hypothesis.
At this point, we want to use the Alloy fact RootHasNoParent as another hypothesis in the proof. This fact is part of the same specification we loaded earlier, and states that the root directory has no parent.
To do this, we type (use "RootHasNoParent") at the Rule? prompt.
This command application opens a new branch in which we will have to be prove that oh_1 is the root directory. On the other hand, to close the current branch we need to use the following fact, that establish the relation between tha parent and the contents of a directory.
As before, this fact is introduced as a new hypothesis by applying the use command.
Now, the hypotheses we have in the current goal can be used to prove that the set denoted by ( (contents . oh_1) . Name) is empty. Would it be the case that this assertion is sufficient to prove that contents . oh_1 is also empty?
We can use the Alloy Analyzer to search for counter examples of that implication. To do this, the command dps-hyp must be used.
Since no counterexample were found, the formula is introduced as a hypothesis in this branch, and a new branch is opened, where this formula is stated as an obligation to be proved.
The current branch can be closed by applying the command (reduce), since no P => lone P is an known property (loaded when the proof begins).
Then, the system automatically shows us the next open branch. In this case, the branch opened when the dps-case was applied.
Now we can use the Alloy assertion Lemma1, present in the specification, as a lemma to close this branch.
To close the next open branch we need to prove that oh_1 is the root directory.
As the sequent formula -1 is part of the conjunction in 1, we only have to focus our effort in prove that the other part of 1 also holds. To do that, we only need to use the predicates that characterize the constant oh_1.
Just by applying the command (prop) this branch can be closed.
Now we have to prove the branch opened when we introduced the case in which oh_1 is the root directory. The following goal can be interpreted as the case in which oh_1 is a directory but it is not the root.
To close this branch, we would like to use the Alloy fact OneParent as a lemma. This fact establish that every directory that is not the root, have exactly one parent.
Since one P => lone P is another pre-loaded lemma, we can close the branch applying (grind). Since there are no others open branches, the proof is completed.