Herramientas Personales
Usted está aquí: Inicio → Investigación → Grupos de Investigación → rfm → Dynamite Proving System → Dynamite Proving System: Main Commands
 

Dynamite Proving System: Main Commands

General Notes

All the PVS commands are available. For example, to exit the tool type the key sequence Ctrl-x Ctrl-c. See the PVS system guide for details.

System Commands

These commands are acceded by holding down the Meta key [1] then pressing x and, after releasing the Meta key, typing the name of the desired command.

  • open-alloy-file -- Loads an alloy specification.
  • prove-alloy-assert -- Begins the proof on the desired assertion. The name of the assertion is asked after the command is executed. Precondition: This command must be executed on the buffer containing the alloy specification being verified.
  • x-prove-alloy-assert -- Same as prove-alloy-assert but initiating the X display.
  • step-proof-alloy-assert -- Begins the proof stepper for the desired assertion. The name of the assertion is asked after the command is executed. Precondition: This command must be executed on the buffer containing the alloy specification being verified.
  • x-step-proof-assert -- Same as step-proof-alloy-assert but initiating the X display.

Proof Commands

As in PVS, the proof commands must be invoked trough the Rule? prompt presented in the *pvs* buffer once the proof begun.

  1. Pretty-printing
    Rule: (disable-alloylike)
    Effect: Deactivates the pretty printing procedures that allows the user to see the proof in Alloy language.
    Rule: (enable-alloylike)
    Effect: Activates the pretty printing procedures that allows the user to see the proof in Alloy language.
  2. Instantiation of Existential Strength Quantifi ers
    Rule: (inst <fnum> [<expr-string>]*)
    Effect: Instantiates the formula indicated by fnum with the given expressions. The command is applied if the conditions stated in the PVS prover guide for the same rule are fulfilled and if the resulting formulas can be typechecked.
  3. Introduction of Cases
    Rule: (dps-case [<formula-string>]*)
    Effect: When the rule (dps-case alpha) is applied on the sequent d_0, ..., d_n |- g_0, ..., g_m, the proof tree grows into two branches with the following sequents:
    1. d_0, ..., d_n, alpha |- g_0, ..., g_m
    2. d_0, ..., d_n |- alpha, g_0, ..., g_m

    representing the spliting of the proof in the case in which alpha stands (1) and the case in which it does not stand (2). Besides that, Dynamite search for instances of the formulas:

    1. d_0 && ... && d_n && alpha
    2. d_0 && ... && d_n && !alpha

    The existence of instances for one of these formulas ensures that the corresponding sequent represents a possible case. If no instance could be found, the case may be empty (ie, no instance can satisfy the hypothesis of the new sequent).

    Observation: the searches are only informative, the rule is applied besides the fact that the instances can be found or not.

    This rule admits a sequence of formulas as parameter. It behaves the same way that the PVS rule case (PVS prover guide, pp. 38), but additionally it searches for instances as explained above.

  4. Full Case Analysis on Formulas
    Rule: (dps-case* [<formula-string>]*)
    Effect: It performs a full case analysis on the given formulas, as PVS command case * does (PVS prover guide, pp. 40), but a search for instance is done on every resulting sequent as explained in the previous section.
  5. Introduction of new hypothesis
    Rule: (dps-hyp [<formula-string>]*)
    Effect: To introduce the formula alpha as a new hypothesis in the proof, the rule (dps-hyp alpha) may be applied. This application on the goal d_0, ..., d_n |- g_0, ..., g_m splits the proof tree in two branches, headed by the following sequents:
    1. d_0, ..., d_n, alpha |- g_0, ..., g_m where alpha is among the hypothesis, and
    2. d_0, ..., d_n, |- alpha, g_0, ..., g_m where alpha must be proved to follow from the previous goal hypothesis.

    When introducing the new hypothesis, Dynamite performs two validating operations:

    1. It searches for an instance of the formula d_0 && ... && d_n && alpha to ensure that it is not an empty case, as in the dps-case command. Thereby, the result of this search does not affect the application of the rule.
    2. It searches for a counterexample of the implication d_0 && ... && d_n => alpha. If the search succeed, the counterexample is shown to the user and the rule is not applied.

    When a list of formulas is given as parameter, the rule behaves as the PVS command case (PVS prover guide, pp. 38).

  6. Valiation of formulas
    Rule: (dps-validate-form <formula-string>)
    Effect: This command validates the given formula by calling the Alloy Analyzer. When a counterexample is found, the Alloy visualizer is used to show it.
  7. Validation of goals
    Rule: (dps-validate-goal)
    Effect: The current goal is analyzed by using the Alloy Analyzer to search for counterexamples of the logical implication implied by the sequent. If the sequent is d_0, ..., d_n |- g_0, ..., g_m, Dynamite searchs for counterexamples of d_0 && ... && d_n => g_0 || ... || g_m. When a counterexample is found, the Alloy visualizer is used to show it.
  8. Simplification of sequents
    Rule: (dps-hide-form <fnum>)
    Effect: Try to simplify the proof goal by hiding the fnum formula and searching for counterexamples of the logical implication underlying the resulting goal. The formula is kept only if that search succeeds. When a counterexample is found, the Alloy visualizer is used to show it.
    Rule: (dps-hide [:mode <uc|it (default uc)>])
    Effect: Hides the irrelevant formulas in the sequent. With the parameter mode you can choose between the UnSat-Core based technique or the iterative technique (see the ICTAC'10 paper for details on the techniques).
  9. Semantic hints to instantiations
    Rule: (dps-seminst <fnum> :vs <validation-scope> :gs <generation-scope> :mr <max-rank> [:terms <max number of terms to generate>] [:elems <max number of semantic elements to work with>] [:ban (<expr>*)])
    Effect: Try to generate an expression that can be used to instantiate the formula corresponding to fnum.
  10. Setting the scopes

    All the searches for instances and counterexamples are performed by the Alloy Analyzer. In every search, the size of the domains (scope) is fixed. The setting of the scopes is done by using the dynamite construct (with-scope <scope-decl> <command>).

    For example, to set 4 as the overall scope to be used in the validation of the current goal, (with-scope 4 (dps-validate-goal)) must be typed at the Rule? prompt.

    The scope-decl accepts the same syntax as the scope declarations in Alloy4.

 

[1] in IBM style keyboards, that is the Alt key.

 

Go back to main page.

Acciones de Documento