Specware 4.0.2

Release Notes

This update package requires that Specware 4.0.1 already be installed on the target machine. If you do not know which version you have, start Specware and look for a “Specware | About Specware” menu item. If it is not there, you have version 4.0 and need to update to 4.0.1 before running this update. If the menu item is there, click on it to view the version of Specware you are running.

This update includes Fixes for two bugs, detailed below.

• Colimit/Import naming bug: If multiple specs are combined (e.g. via imports or colimit) and they refer to sorts or ops with overlapping sets of names (e.g. {A,B,C} and {A}), the resulting spec may erroneously duplicate the problematic sort/op, e.g.:

  sort {A,B,C}
  sort {C,B,A}
  

  References to overlapping sets of names now get correctly processed.

• Snark prover interface bug: Snark deals with propositional symbols differently than predicate symbols and the previous translation failed to take this into account, resulting in unexpected error messages. Propositional symbols are now handled properly.