Dynamite Proving System: Release Notes

Version 0.2.2.1 (Aug. 20th., 2011)

New features

• Alloy subset signatures are now supported.
• Domain and range restriction operations (<: and :>) are now supported.
• Every proof rule attempt is logged in the file proof-logging.csv.

Bug fixes

• Variable names in translation of domain constrains does not contain / anymore.
• Messages of dps-validate-goal proof rule were corrected.

Version 0.2.2.0 (Jul. 17th., 2011)

New features

• The proof commands were revisited and improved.
• The scopes for the validations are now stated using the (with-scope <scope-decl> <rule>).

See the manual for details.

Version 0.2.1.12 (Apr. 29th., 2011)

New features

• The instantiation commands inst-cp, instantiate and instantiate-one now accepts alloy terms (like inst does).
• Now, the instantiations attemps by means of any command (inst, inst?, inst-cp, instantiate and instantiate-one) are applied only if the resulting formulas can be typechecked.

Version 0.2.1.11 (Dec. 12th., 2010)

New features

• New user commands: x-prove-alloy-assert, step-proof-alloy-assert and x-step-proof-alloy-assert.

Bug fixes

• The prover commands expand and flatten (and hence prop) now simplify the negated operators !in and !=.

Version 0.2.1.10 (Dec. 7th., 2010)

New features

Usability improvements:

• The pvs specification files, where the underlying PDOCFA theory is modeled, are no longer showed as side efect of a proof intent.
• The proof comands were renamed. See the manual for details.

Version 0.2.1.9 (Nov. 1st., 2010)

New features

Usability improvements:

• Syntax highlighting for Alloy files.
• Auto-complete of assertion names for the command prove-alloy-assert.

Version 0.2.1.8 (Oct. 19th., 2010)

New features

Usability improvements:

• The command load-alloy-spec is replaced by the command open-alloy-file.
• Specific Dynamite user menu is added.

Version 0.2.1.7 (Aug. 24th., 2010)

New features

• The UnSAT-core suggestions are now higlighted on the Alloy model buffer. Use <s-up> and <s-down> to navigate between suggestions.

Version 0.2.1.5 a.k.a Dynamite 2.0 (April 6th., 2010)

New features

• The prover command dps-hide tryes to prune the current goal by using an UnSAT-core extracted from the sequent.

Version 0.2.1.4 (March 29th., 2010)

New features

• The prover command dps-prune tryes to prune the current goal by iteratively searching for counterexamples of the goal without a formula in turn.

Minor changes

• Cambia la forma de sintetizar goals. Ahora sólo se usan facts y run{}.
• Se agrega al comando proof-status la posibilidad de indicar de los elementos de los que depende la demostración, cuáles se usan directamente en ella.

Version 0.2.1.3 (February 19th., 2010)

New features

• Improvement of matching procedures. The command inst? now can find instantiations that previously were ignored, by using the axioms that imposes constrains on the constants.
• The prover command dps-validate-goal offers suggestions on the use of lemmas, parts of the specification and formulas in the sequent, to close the goal.

Minor changes

• Se agrega el comando de usuario M-x show-dps-lemmas que muestra las declaraciones de "asserts" y "facts" propios de la especificación que están disponibles para ser usados en las demostraciones.
• Mejoras en la interfaz entre el demostrador y el traductor. Se mejora el proceso de los argumentos de línea de comando del traductor. Se modifican consecuentemente los procedimientos que forman parte de la interfaz de DPS con el traductor.

Version 0.2.1.2 (December 1st., 2009)

New features

• Every validating proof command runs automatically the Alloy counterexample visualizer when a counterexample is found.
• The scope of the searches can be indicated in every validating proof command (see the brief manual for details).
• The automatization in proofs of TCCs has been improved.
• The proof commands dps-enable-alloylike and dps-disable-alloylike are now recorded in PVS proof files (.prf).

Version 0.2.1

• Support for Alloy 4-1-10 (Alloy3 is no longer supported).
• Dynamite is now based on PVS 4.2.
• The Alloy modifier disj is supported.

Version 0.1.1

• Tutorial released.
• Improvement in pretty printer (minus operator).
• General lemmas added:
  • no P => lone P
  • one P => lone P