README file for Escher Verification Studio version 6.10.01

CONTENTS

0.	Version Identification
1.	Platform Requirements
2.	Installation
3.	Documentation
4.	Editor customization
5.	Running the examples
6.	Reporting a problem
7.	Target language compilers
8.	Updates
9.	Known issues
10.	Acknowledgments

APPENDICES

A.	Changes since Escher Verification Studio 6.01
B.	Changes since Escher Verification Studio 6.0
C.	Changes since Escher Verification Studio 5.10
D.	Additional changes since Perfect Developer version 5.0

0. VERSION IDENTIFICATION

This Readme file is for Escher Verification Studio release 6.10.01. File versions are as follows:

	VerificationStudio executable	6.10
	EscherTool executable		6.10.01
	builtin.pdc			6.10.00.00
	ecv.pdc				6.10.00.00
	rubric.pdc			6.10.00.00
	Documentation			6.10 (some files) and 6.0 (remaining files)

1. PLATFORM REQUIREMENTS

Escher Verification Studio is intended to be installed on a PC with a 1GHz or faster processor, at least 3Gb of memory, and a Windows XP, Windows Vista, Windows 7, Windows 8 or Linux operating system. If you intend not just to verify specifications but also to build applications, you will need the Sun Java SDK version 1.6, or a C# version 2.0 or later compiler, or a C++ compiler (see our web site for C++ compiler compatibility information).

2. INSTALLATION

The following notes refer to installation under Windows. For installation under Linux, see the separate readme-linux.txt file.

If you have a version of Perfect Developer or a version of Escher Verification Studio 5 installed, you can leave it installed on your computer if you wish. Escher Verification Studio 6 uses a different directory and registry key structure, so the two installations will not interfere with each other. You may import projects developed with Perfect Developer into Escher Verification Studio; however, once a project has been saved by Escher Verification Studio, you may subsequently find that Perfect Developer cannot open it.

To install Escher Verification Studio from a CD or other distribution media, insert the CD into the drive. If the install program does not start automatically, open My Computer or Windows Explorer, then browse to the CD and run the file Autorun.exe. If instead you have downloaded Escher Verification Studio as a Microsoft Installer (.msi) file, just run the file.

3. DOCUMENTATION

The following documents are installed in HTML and/or PDF format:

•	User Guide describes how to use the Project Manager, which is the main user interface to Escher Verification Studio.

•	Perfect Developer Language Reference Manual describes the Perfect language.

•	Escher C Verifier Reference Manual describes how to write C programs that conform to the eCv subset of C, and how to annotate them so that eCv can verify them.

•	Development Overview gives guidelines on how to develop software systems using Perfect Developer.

•	Language Introduction introduces the Perfect language by way of examples. A more comprehensive introduction is to be found in the tutorials on our web site at http://www.eschertech.com/support/perfect_developer_self_help.php.

•	Creating a Java application using Perfect Developer and the JDK describes how to build an application using Perfect Developer compiled to Java.

•	Interfacing a Java graphical user interface to a Perfect application follows on from the previous document, explaining how to attach a Java graphical front-end to a Perfect application.

•	Verification Conditions generated by Escher Verification Studio describes the various types of verification condition that you will see the system trying to prove, and what they mean.

Other documents (including a tutorial on the Perfect language) are available on our web site via the Support link.

4. EDITOR CUSTOMIZATION

Escher Verification Studio includes a built-in editor. Alternatively, you can configure the Project Manager to invoke a third-party editor of your choice. This configuration mechanism is accessed via the Options menu of the Project Manager.

If you will be writing specifications in Perfect and using a third-party editor then we strongly recommend that you use an editor that supports syntax highlighting for the Perfect language. To this end, we provide editor customization files for a number of popular editors (XEmacs, Vim, Multi-Edit 11, TextPad, Emerald/Crimson and Kate). For each editor, you will find the customization files in an appropriate subfolder of the Editor Customizations subfolder of the Escher Verification Studio installation directory, together with a Readme.txt file explaining how to use them.

If you will be writing C or C++ programs for verification by Escher C Verifier, then we strongly recommend that you extend the syntax highlighting implemented in your editor by adding the extra eCv keywords (perhaps highlighting them in a different color from regular C/C++ keywords). You will find these keywords listed in Chapter 2 of the Escher C Verifier Reference Manual.

5. RUNNING THE EXAMPLES

The Examples subfolder of the installation contains further subfolders, each of which provides one or more examples of how Perfect Developer or Escher C Verifier can be used. The Perfect Developer examples are:

•	HelloWorld shows how to build a simple console-mode application using either Java or C++ as the target language.
•	General provides three simple class-based examples of specification: Date, DictionaryUnrefined and QueueUnrefined.
•	Refinement comprises a number of examples. Factorial and Loop demonstrate algorithmic refinement, while Dictionary and Queue demonstrate data refinement of the corresponding classes in the General folder.
•	Graphical shows how to construct an application using a Java/Swing user interface connected to a Perfect back-end. It uses a copy of the Dictionary example from the Refinement folder for the back-end, wrapping it with a "firewall" to guard against user input that does not meet the appropriate preconditions.
•	Mondex is a translation from Z of the Abstract World part of the specification of the Mondex electronic purse.

The Escher C Verifier examples are:

•	ecvPlatformCheck.c is a simple file to verify that the integral type sizes you have specified for your C/C++ compiler match the values found in header file limits.h.
•	bsearch.c and bsearch.h demonstrate specifying a binary search function for full functional verification.

All these examples can be 100% verified by Escher Verification Studio, but depending on the speed of your computer, you may need to extend the verification timer and boredom limits (especially for the Mondex example). For the HelloWorld and Graphical examples, project files are included so that you can build a complete application.

6. REPORTING A PROBLEM

If you encounter a problem with Escher Verification Studio , please check the following before reporting it or requesting support:

•	You are using a compatible operating system and hardware platform;
•	The problem is not already listed as a known limitation in this document or on our web site.

Report Escher Verification Studio problems using the problem report form on our web site http://www.eschertech.com.

7. TARGET LANGUAGE COMPILERS

See the support section of our web site (http://www.eschertech.com) for a list of C++ compilers that have been used to compile code generated by Perfect Developer. We have additional resources available for those wishing to interface handwritten C++ code to code generated by Perfect Developer; please contact us for details.

8. UPDATES

From time to time we may make software updates available for download. Notice of availability of such updates for the free edition will be given in our email newsletter. You need to have opted-in to receive this newsletter.

9. KNOWN ISSUES

A full list of known issues is available to commercial customers with a current support contract. This section just lists the ones that are most serious and/or most likely to be encountered.

(a) Compiler/verifier issues

890 (Perfect Developer only): The verifier does not attempt to prove that integer values in a computation are within the bounds of the types used in the generated code. Therefore, a specification may be successfully verified, yet the code may fail to execute correctly if overflow occurs. Workaround: (1) do not declare variables of type int or nat, instead declare your own subtypes of int, ensuring that the entire range if your subtype can be represented in an integer variable of your target language; and (2) in arithmetic expressions with more than one operator, wherever there is the possibility of overflow you can force the generation of a verification condition that an intermediate value is in range, for example by passing it to a function whose input type is suitably constrained.

1136, 1137: Verification of floating-point computations uses axioms applicable to idealized real numbers, rather than the limited-precision floating-point types available in the output language. Therefore, verification of programs that use floating point arithmetic is not sound in this version of Perfect Developer and Escher C Verifier.

1138 (Perfect Developer only):  If your program uses explicit references, then it is possible to construct a situation in which there are circular chains of explicit references, or circular chains of explicit and implicit references. In this situation, it is possible that within a class method body, you make a call to a method in another class that eventually calls another method in the original class. Under these conditions, the verifier does not recognize that the class invariant of the original object may not be satisfied when this last call is made; therefore, verification is unsound in this situation.

1139 (Perfect Developer only):  If your program uses explicit references, then it is possible to construct a situation in which there are circular chains of explicit references, or circular chains of explicit and implicit references. The reference-counting garbage collector used in generated C++ code will not reclaim cycles of objects.

1185: (Perfect Developer only):  Although Perfect Developer can read UTF-8 source files and uses a 16-bit or larger character set internally, generated code files are written in ASCII; therefore Unicode characters cannot safely be used in character and string literals when generating code.

1264: When generating a cross-reference listing, if a generic class or method has a require-clause of the form 'require X has $' where X is a class parameter and $ is a method or constructor, and that generic class or method is subsequently instantiated with class T in place of parameter X, then method $ in class T should be assumed to be referenced. However, it isn't; which means that method $ in class T may be flagged as 'unreferenced' if it isn't used anywhere else.

1281: (Escher C Verifier only): eCv doesn't allow structs or unions to have anonymous members, except that structs may have anonymous bit fields to represent padding.

1285: (Escher C Verifier only): The semantics of the C 'goto' statement are not fully handled. Typically this means that verification conditions generated for code that follows a label that is the target of a 'goto' cannot be proven.

1288: (Escher C Verifier only): Instances of indirection through pointers whose targets are local variables that have gone out of scope are not detected.

1322: (Escher C Verifier only): Instances of uninitialized out-parameters are not detected

(b) Project Manager issues

1140: When the proof or unproven output file format is set to HTML, it is intended that you can right-click on a warning or information message in the Output window and select Go to proof information. However, when the default browser is Internet Explorer 7 or 8, this takes you to the head of the HTML file, not to the correct bookmark in the file. This is a limitation of IE7 and IE8. We do not know of any workaround other than to use a different browser such as Firefox.

10. ACKNOWLEDGMENTS

We wish to thank the following for their contributions to the Escher Verification Studio package:

•	All those who contributed to wxWidgets - a professional, open source, cross-platform graphical user interface library;
•	All those who contributed to the Scintilla open source editor component;
•	All our beta testers.

APPENDIX A: CHANGES SINCE ESCHER VERIFICATION STUDIO 6.01

(a) Changed behaviour

159: The sequence of locations in which eCv searches for a file referred to in a #include directive has changed to bring it into line with major compiler vendors. If the filename is enclosed in angle brackets, eCv now looks only in the project include paths and then the compiler include paths. If the filename is enclosed in double-quotation marks, then eCv looks first in the directory containing the including file, then the directory of the file that included that one, and so on until the original source file is reached; then it looks in the project include paths, and finally in the compiler include paths.

161 (PD only): name, public and external may no longer be attached to identifiers and are not reserved words. Use of these keywords was previously deprecated. Use the corresponding pragmas instead.

(b) New features

153, 154 (eCv only): eCv now supports a wider range of C++ constructs, including nonstatic class member functions, constructors, inheritance, virtual functions, and overriding. This support is still experimental. A new chapter in the eCv manual describes the C++ support.

155 (eCv only): Some constructs from C++ 2011 are now supported.

156: (PD only): Trace-statements may now be conditional. See the Language Reference Manual for details.

158: (eCv only) Escher C Verifier now recognizes directives of the following form:

 #pragma ECV ignore_warning $ "warning text 1", "warning text 2" ...

where $ is an optional integer (defaulting to 0 if omitted), and "warning text 1" etc. are parts of warning messages. The effect is that for each of the specified warning texts, a single instance of a warning message containing that text generated $+1 lines further on will be ignored. An informational message will be generated that the warning was ignored. If no matching warning message is seen, a warning message will be generated.

160 (PD only): The runtime library class Environment now contains new member getRuntimeLanguage.

162: The editor built in to the Project Manager now has additional right-click menu items to find definitions of the identifier under the cursor, and to find references to the identifier under the cursor. The find-definitions function (shortcut key ctrl-D) searches for class, function, schema and selector declarations if you are editing a Perfect source file, and searches for type declarations only if you are editing a C or C++ file. It searches all files in the project and included or imported files. It is not completely accurate, especially in C and C++ source files. The find-references function (shortcut key ctrl-alt-F) looks for case-sensitive whole-word matches of the identifier in all files in the project and included or imported files. Occurrences and definitions within comments are generally not reported.

163: When you right-click on a tab in the editor, the pop-up menu has a new option to sort the tabs into alphabetical order by filename. This makes it easier to find the correct file when you have a large number of files open in the editor.

164 (eCv only): Non-ghost functions and constructors may have additional ghost parameters.

(c) EscherTool bug fixes

1361 (eCv only): If an enumeration was defined inside a class, then the enumeration constants couldn't be accessed via the class scope resolution prefix.

1362 (eCv only): Use of the va_start macro always provoked a warning of possible invalid verification results due to an unsafe cast.

1363 (eCv only): An eCv pragma in header file ecv.h caused some compilers to report an "unrecognised pragma" warning.

1364 (eCv only): Given a typedef that names a function pointer type, in a declaration that type name may be suffixed with "null" to declare a nullable pointer of that function type. However, in a C-cast or static_cast, using "null" after the type name gave rise to a syntax error message.

1365 (eCv only): When processing C++ source, eCv did not allow a file-scope identifier declared as 'const int' to be used in the bound expression of an array declarator.

1366 (eCv only): When a typedef declared a const pointer type, then if the typedef-name was used with a null-qualifier to declare a nullable pointer, the const-qualification was lost.

1367 (eCv only): Functions snprintf and vsnprintf write through their first arguments, however their declarations in stdio.h did not have writes-clauses.

1368 (PD only): A recursion variant of the form "decrease n' " (when n is an in-out parameter) is not permitted because of the prime; however no warning was generated.

1369 (Critical, PD only): The C# code generated for equality of an expression of type T || void with an expression of type T (where T is an enumeration type) always yielded false.

1370: Under certain conditions, the prover was unable to generate a refutation from terms "forall x::S : ~(x = A)" and "A in S", where A is a literal and S is a non-literal set.

1371 (PD only): If a method in the abstract section of a class was preceded by one or more invariants and followed by two or more comma-separated invariants, then some invariants that precede the method were ignored when deciding what 'class invariant preserved' VCs to generate, what givens to assume, and what class invariants to assume when the method is called. This typically caused the methods concerned and/or methods that call them to fail to verify.

1372 (PD only): Assertions embedded in some types of postcondition (e.g. pass) were not used to generate state information, so these assertions did not help with subsequent proofs as they should.

1374 (eCv only): The declaration "T (*id)[n]" declares id as a pointer to an array having elements of type T. However, eCv treated it as declaring an array of n pointers to T, just as if we had said "T *id[n]".

1375: In debug output and proof output, type expressions were sometimes printed without the required brackets. For example, type "(fseq of int)*" is printed as "fseq of int*".

1376 (eCv only): If there is a forward reference to a variable whose type contains an array whose bound is the value of a "const int" declared earlier, then EscherTool would terminate unexpectedly because the array size was used before it was bound.

1377 (PD only): If an expression of the form v! = v.f(e) was rewritten by the user as v!f(e) using the new facility to do this in PD version 6, then the prover was no longer able to prove properties that it was able to prove prior to the rewrite.

1378: If a quantified expression had literal bounds, then under certain conditions this led to the prover declaring some truths unprovable.

1380 (Critical, eCv only): The invariant of a C/C++ enumeration type used to be that the value must match one of the declared enumeration constants. However, the precondition of the constructor from int only required that the value lie between the lowest and highest constants inclusive. Similarly, the precondition of the increment and decrement operators only required that the value is not already at the end of the range. So the invariant was inconsistent with the preconditions. The invariant has been changed so that the value need only lie between the lowest and highest values inclusive.

1381 (eCv only): eCv assumed that the lowest value of an enum was the first constant declared, and the highest value was the last constant declared. This is not necessarily true for C and C++ enums.

1382: The implementation of the prover rule "expand literal quantifiers" often failed to notice terms that it could be applied to, which could lead to failed proofs.

1383 (PD with Java code generation only): The Java runtime library did not include support for the trace facility added in release 6.

1384 (PD with C# code generation only): If toString was applied to a union with void (either explicitly, or by including an expression of a union-with-void type in a trace statement), then the generated C# code referred to a missing function and would not compile,

1386: The term index failed to find some matching terms when the search term was a binary commutative but non-associative operator and one of the operands was a literal rule parameter. This may have led to failed proofs.

1387 (eCv only): In a typedef for a function type, ghost operators were not permitted within the specifications.

1388 (Critical, eCv only): If a conditional expression yielded a function pointer, and this pointer was used in a context requiring a particular function type, then the verification conditions asserting that the expression type satisfied the Liskov Substitution Principle with respect to the expected function pointer type were incorrect.

1389 (eCv only): If a declaration of an array of function pointers had an initializer, and the type of the function pointer had a writes-clause containing a not_null expression, then EscherTool would terminate while generating the verification conditions.

1390 (eCv only): If a function declaration had a parameter with type pointer to pointer to function, and the type of the function pointer had a writes-clause containing a not-null expression, then EscherTool would terminate while generating the verification conditions.

(d) Project Manager bug fixes

1391: When the Replace in Files dialog was used, after a match was found in a new file, the Replace, Find Next button and Replace All button were sometimes greyed-out.

1392: When the Replace All button was pressed, if the search string was a substring of the replace string then the editor would become unresponsive because it was recursively replacing text.

1393: If a Find in Files or Replace in Files menu option or keyboard shortcut was used when there were no files open in the editor and the Search/Replace dialog had not yet been shown, then the Search/Replace dialog would be drawn too far to the left such that only part of it was visible.

APPENDIX B: CHANGES SINCE ESCHER VERIFICATION STUDIO 6.0

(a) New features

eCv now supports static member variables of C++ classes.

eCv now enforces 'private' and 'protected' C++ class member access specifiers.

The Perfect exponentiation operator is now available when writing eCv specifications, with name _ecv_pow.

1350: eCv now allows a switch-expression to have Boolean type, however this will give rise to a warning because it is not MISRA-compliant. This feature was added to support code generated by Simulink.

1356: eCv now supports compliance checking against many of the MISRA-C-2012 rules. The user can choose between MISRA-C 2004 and MISRA-C 2012 rules.

(b) EscherTool bug fixes

1344: eCv now allows "typedef void Void" and similar typedefs for void.

1349 (eCv only): If all the cases in a switch-statement were block statements, and each block was terminated by a break-statement inside the block, then eCv incorrectly reported that the statement following the switch-statement was unreachable.

1354 (eCv only): If a function returning a float or double had a returns-annotation, a spurious type conversion warning was generated.

1359 (Perfect Developer only): If a schema call binds to a function used as a schema, and there is an optimised schema version of the function available, then code generation sometimes failed with an absurd function call reported.

1360 (eCv only): If a static member function was declared in a class and defined at the point of declaration, then an attempt to access the static member from outside the class using the scope resolution operator failed.

(c) Project Manager improvements and bug fixes

1347: A minor layout issue in the Compiler Definition dialog has been fixed.

1351: When an eCv project is open, the editor Open File dialog now includes .h and .hpp extensions in the default file type filter.

1356: In the Options -> C/C++ Compilers dialog, the buttons used to edit the list of include paths would disappear when using long include paths.

1357: The "Save a copy as..." editor function did not allow a copy to be saved when the original file was read-only.

1358: The "Save a copy as..." editor function incorrectly set a save point.

(d) Library improvements and bug fixes

1345: When the eCv compiler type is set to C++, stdlib.h and math.h now provide extra overloads for some functions as required by the C++ 2003 standard.

1346: eCv now provides standard include files cstddef, cstdlib, cmath etc. that are equivalent to the C languags standard header files, for use with C++ source code.

1348: eCv specifications are now provided for library functions abs, fabs, pow and ldiv.

APPENDIX C: CHANGES SINCE ESCHER VERIFICATION STUDIO 5.10

(a) New features and improvements

1304 (Escher C Verifier only): If MISRA-C 2004 checking was enabled, eCv used a strict interpretation of the implicit signed/unsigned conversions rule and warned about implicit conversions of signed integer literals to unsigned. This has now been relaxed so the the warning is no longer generated, provided that the integer literal will fit in the type to which it is being converted.

1307 (Escher C Verifier only): If a non-nullable pointer is compared with NULL, the error message generated now suggests that a null qualifier may have been omitted.

1310 (Escher C Verifier only): The grammar now permits a trailing semicolon after a global assertion or assumption.

1324: If the wrong version of the builtin.pdc, ecv.pdc or rubric.pdc file is used then a better error message is now produced.

147: When the parser detects a syntax error, a list of valid continuation token types is included in the error message.

148: Error and warning messages can now span multiple lines. When the verifier generates suggestions, these are now included in the warning message.

149 (Perfect Developer only): the trace statement is now supported. See the Language Reference for details. The debugPrint function is now deprecated.

150 (Perfect Developer only): a member function that returns an object of the same type as self can now be called as if it is a schema modifying self. An optimized version of the schema form can be re-implemented in the internal section (similar to the way in which assigning operators such as !+ can be re-implemented).

151: The prover speed has been improved through increased use of expression indexing.

152 (Escher C Verifier only): Some more C++ constructs are now supported when the source language is specified as C++ in the compiler settings. See the eCv Reference for details.

118: The Project Manager now has a built-in editor.

(b) Documentation improvements

1308 (Escher C Verifier only): The section of the reference manual dealing with loops now includes a complete list of loop annotations and indicates the required order of them.

1309 (Escher C Verifier only): The correct positioning of contracts in function prototypes has been clarified in the documentation.

(c) Bug fixes

1297, 1298: (critical, Perfect Developer when generating C# or Java code only): If a schema took a non-limited in-out parameter of type (T || void) where T is some class type, then incorrect code was sometimes generated when calling the schema.

1299: (Perfect Developer when generating C# or Java code only): If a Perfect source filename contains non-alphanumeric characters, then the name chosen for the automatically-generated wrapper class could contain characters that are not legal in an identifier, and the code would not compile.

1300: The global swap schema in the C# and Java libraries for code generated by Perfect Developer was not correctly named in the library, so generated code using it would not compile.

1301: (Perfect Developer only): If a specification called the toString member function on an expression whose type is a union with void, the prover might terminate abnormally with an assertion failure.

1302, 1319: When converting the proof steps to human-readable form for output to file, some branches of the proof were sometimes omitted.

1303: If a proof involved a function call inside a forall-expression, the function had no result expression (PD) or returns-specification (eCv), the prover failed to make use of the function postcondition when searching for a proof.

1305 (Escher C Verifier only): VT and FF characters were not accepted as white space.

1306 (Escher C Verifier only): In an enumeration declaration, eCv did not allow an enumeration constant to be defined as equal to another one, unless the unary '+' operator was used to convert it to integer type or a similar workaround was used.

1311 (Escher C Verifier only): The prover was unable to determine the limit of a void* pointer cast to a char* even when the limit of the void* was known.

1312 (Escher C Verifier only): Under some conditions the prover was not able to prove that the precondition of printer arithmetic was satisfied even when such a proof should have been simple.

1313 (Escher C Verifier only): If a function writes-clause specifies that only part of the object pointer to by a parameter was written, and the function is called with the parameter pointing to a local variable, then eCv reported that the call was not permitted.

1314 (Escher C Verifier only): If NULL was passed to a function requiring an out-parameter of nullable pointer type, then eCv reported that the call was not permitted.

1315 (Escher C Verifier only): If an array with automatic storage duration was passed to a function requiring an out-parameter of nullable array pointer type, then eCv reported that the call was not permitted.

1316 (Escher C Verifier only): The prover was unable to reason about the value of an expression of type int cast to char.

1317 (Perfect Developer only): If the inherits-part of a constructor throws exceptions, then PD warned that the constructor was not declared as throwing exceptions of that type even when it was.

1320 (Escher C Verifier only): A constant or parameterless function called aa could not be declared if there was an enumeration declaration in the same scope.

1321 (Escher C Verifier only): If a pointer was cast to void* using a C-cast or a static_cast then the prover was unable to reason about the size of the object addressed by the resulting pointer.

1325 (Escher C Verifier only): If an expression in a function writes-clause is not a potentially writable object, then under some conditions eCv would terminate abnormally before reporting the error.

1326 (Escher C Verifier only): When a parameter of multidimensional array type is declared, eCv was not checking that bounds information had been given for all array dimensions except (optionally) the first.

1327 (critical, Escher C Verifier only): When a parameter of multidimensional array type is declared, eCv did not generate verification conditions that all calls to the function have the correct bounds for the second and later indices.

1328 (Escher C Verifier only): eCv occasionally generated suggestions containing expressions that were not valid C syntax.

1329 (Escher C Verifier only): eCv occasionally generated meaningless suggestions that proposed adding preconditions referring to local arrays.

1330 (Escher C Verifier only): eCv occasionally generated a pedantic warning that type integer has been converted to int.

1331 (Perfect Developer only): If a regular class defines a member operator, and the schema version of that operator is re-implemented in the internal section, and the operator symbol translates to a symbol (not an identifier) in C++, then incorrect code is generated when the schema is invoked and the code will not compile.

1332 (critical, Perfect Developer when generating C# code only): If a schema has an out-parameter whose type is a regular class, and the schema assigns a value to the parameter and subsequently calls a member schema on it, incorrect code was generated that could result in incorrect object aliasing.

1333 (Perfect Developer only): PD did not ensure that an overriding method in a derived class throws no more exception types than the overridden method does.

1334 (Perfect Developer only): PD did not ensure that exception specifications cannot declare that constrained types are thrown.

1335 (Perfect Developer only): If a schema with an out-parameter initializes it by calling another schema having an out-parameter of a narrower type, and subsequently reads the out-parameter, then a spurious and suppressed error is generated.

1336: Calls to Environment caseSensitiveFileNames  in the Java library for code generated from Perfect Developer returned true even under Windows.

1337: The prover sometimes incorrectly classed terms as irrelevant, leading to failed proofs.

1338 (critical): Prover sometimes made incorrect inferences after determining that a set or bag contained exactly one element.

1339: No warning was given if the predicate in a 'that', 'any' or 'those' expression did not depend on the bound variable.

1340: No warning was given if the predicate in a 'forall' or 'exists' expression was an opaque expression.

1341 (Perfect Developer only): If nested when-guards were used when declaring abstract data, all but the outermost when-guards were discarded without warning. Nesting of when-guards is no longer permitted.

1342: The prover sometimes failed to try unifications involving less-than terms, leading to failed proofs.

1343: The axiomatisation of the ** operator between maps and sets in the theorem prover was incomplete, which often resulted in failure to prove theorems using this operator.

APPENDIX D: ADDITIONAL CHANGES SINCE ESCHER VERIFICATION STUDIO 5.0

(a) Bug fixes

1289: If a proof list is attached to a schema postassertion, it may need to refer to primed variables. However, within conditional proof list items, EscherTool reports that the primed variables concerned have no distinct instance.

1290: We have an example involving proof lists for which EscherTool terminates unexpectedly while generating VCs.

1292 and 1294 (critical): If a schema is expanded multiple times, and the schema postcondition contains variable declarations, then the values of the variables in the different expansions may get mixed up, which can lead to incorrect proofs.

1293: If a specification includes a recursive schema then eager expansion of calls to that schema may never terminate. This may prevent other prover rules being used, leading to failed proofs.

1294: A few prover rules such as "++ over nested for..yield" were no longer working because of a change in version 5.0.

1295: Matching the second term in term-combining rules such as "transitivity 1" was unnecessarily slow and could lead to prover timeout in some situations.

Escher Technologies Limited, 16 January 2014.