README file for Escher Verification Studio version 6.0

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 5.10
B.	Additional changes since Perfect Developer version 5.0
C.	Additional changes since Perfect Developer version 4.10.02
D.	Additional changes since Perfect Developer version 4.0

0. VERSION IDENTIFICATION

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

	VerificationStudio executable	6.03
	EscherTool executable		6.03
	builtin.pdc			6.0
	ecv.pdc				6.0
	rubric.pdc			6.03
	Documentation			6.0

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.

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;
•	Tarma Software Pty Ltd. for providing the Autorun.exe file;
•	All our beta testers.

APPENDIX A: 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: 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 B: 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.

APPENDIX C: ADDITIONAL CHANGES SINCE PERFECT DEVELOPER VERSION 4.10.02

(a) Product name change

Perfect Developer has been subsumed into Escher Verification Studio. File names and paths have been changed as follows:

•	The main installation directory is now
[PROGRAMFILESDIR]/Escher Technologies/Verification Studio 5 instead of [PROGRAMFILESDIR]/Escher Technologies/Perfect Developer

•	Example files are installed to 
[PROGRAMDATADIR]]/Escher Technologies/Verification Studio 5 so that they can be written even under Windows Vista and Windows 7

•	File PerfectDeveloper.exe is replaced by VerificationStudio.exe

•	File PDTool.exe is replaced by EscherTool.exe

•	Registry entries are written under the key 
Software/Escher Technologies/Verification Studio 5 instead of 
Software/Escher Technologies/Perfect Developer

Escher Verification Studio includes both Perfect Developer and Escher C Verifier, with options to install either product or both. Depending on the edition of Escher Verification Studio that you have, one or other product may have a capacity limit or reduced functionality.

Additional command line options have been added to EscherTool to support verification of C programs. See the User Guide for details.

(b) New and modified features

Compared to previous releases, this version of Perfect Developer sometimes produces fewer
verification conditions than version 4.10.02. The 'missing' verification conditions are of type Only variables modified in specification are modified by implementation, and the conditions they used to express are now included as extra conditions within the verification condition of type Specification satisfied at end of implementation that is generated at the same location.

New options to generate a Verification Report and control its features have been provided. This replaces the option to write error messages to a file.

The Project Manager no longer provides the option of writing the proofs for all files in a verification run to a single common file. Likewise for the 'unproven' information. The corresponding EscherTool command line options -vpf and -vuf are withdrawn.

EscherTool no longer supports the obsolete command line option -vo. Use -vp to enable proof output and -vu to enable 'unproven' output.

PDTool command line option -p has been changed to EscherTool option -mp.

When the output format for proof files, unproven information or the verification report is set to Tex, the output files are actually generated in LaTeX format. This allows you to use the pdfLatex program from the popular MikTex suite to generate PDF files. A global configuration option is provided to set the page geometry when generating LaTeX. Previously, you had to use pdfTex, which failed on large files and produced less readable results.

(c) Perfect Developer compiler/verifier improvements and bug fixes

145: Command line option -ef=filename now causes a Verification Report to be generated, instead of writing error messages to file. The report format can be selected using new command line option -ey.

1224, 1228, 1229, 1232, 1243, 1253, 1271, 1273: Various prover issues that sometimes led to poor performance or failed proofs have been fixed.

1231 (critical): The prover could incorrectly infer that a collection was non-empty when trying to prove an 'exists' expression.

1233: Expressions involving the internally-used 'dynamic_type' operator sometimes appeared in suggestions.

1234, 1235: When C# code generation is used and generation of debug checks in enabled, the generated C# code may not compile because some overridden functions are not declared 'virtual'.

1236: When class invariant checks are enabled in code generation, some of these checks may recurse until the nesting limit is reached, resulting in poor performance.

1237: In a non-final class, the compiler/verifier requires that only early members of 'self' may be called in invariants. However, in final classes this restriction was relaxed. This means that it is possible for the invariant of a final derived class to call a non-early member of a parent class that is overridden in the derived class, so that the invariant calls a function that assumes the invariant; or it could call a member of a parent class that in turn calls a member that is overridden in the derived class. The compiler will now generate an error message if a class invariant calls a function that assumes that same invariant.

1242: If a generic class was instantiated with a class parameter of type 'ref from limited X on H' for some type T and heap H, then the generated Java code would not compile.

1249 (critical): Evaluation of expressions of the form 'a % b' in the prover sometimes gave incorrect results when 'a' was a negative integer literal.

1250: The prover now knows that unequal characters are mapped to unequal integers by the unary + operator.

1244, 1245 (critical): The prover internal checks for correct quantifier depths in prover rules were incomplete for some types of prover rule. Some prover rules relating to expressions containing nested bound variable declarations were found to have incorrect quantifier depth adjustments. This typically led to prover termination due to a type error or to failed proofs, but could possibly lead to false proofs.

1246: Under some circumstances, generated C++ code would not compile because additional #include directives were needed.

1247, 1248: When generating Java or C# code, if a member of an enumeration class in the Perfect source had a name that was a Java or C# reserved word, then the result of calling 'toString' for that value was the mangled name instead of the original name.

1253: If a templated class declaration inherited a non-templated class explicitly, then the prover could terminate unexpectedly when trying to verify specifications involving the templated class.

1254 (critical): If a base class declared operator ~~ but a class derived from that base class did not, the prover could incorrectly assume that all values of the derived class rank same.

1257: If a schema in-parameter contained as is-cast, and the subject of the is-cast was potentially aliased to an in-out parameter of the schema, then the generated code could be incorrect. In these cases, the generated code does not compile because of type errors.

1258: If a primitive type or value of small class type is converted to a union in a context in which a pointer is required (e.g. as a function parameter), then a small amount of memory could be leaked by the generated C++ code.

1260: If unproven output is enabled and the selected format for it is plain text, the verifier could hang while generating the unproven output.

1263: Immediately after applying a rewrite rule relating to a for..yield or that/those/any expression, the operand of a deBruijn manipulator expression introduced by the rewrite rule could be rewritten by an in-bounds rule prior to the manipulator being evaluated, resulting in failure to find the proof.

1265, 1266, 1267: In rare circumstances conflicting rewrite rules could be generated, causing the proof attempt to be abandoned.

1268: When trying to verify a schema defined as 'post ?' a "Specification is incomplete" warning is now generated.

1270: If a derived class has an internal class invariant, the prover generally fails to prove that this invariant is preserved by inherited schemas, even if it is.

1272: The prover sometimes used large amounts of memory while attempting unification, ignoring the configured memory limit.

1276: When proof output was enabled, the proofs sometimes included the development of terms that were not subsequently used.

1283: If the prover found two or more refutations in the same inherited class context, it sometimes terminated unexpectedly while generating 'unproven' output.

(c) Project Manager changes and bug fixes

137: The temporary file used to pass the input file list from the Project Manager to the compiler/verifier is now created in the system temporary directory and has a unique name instead of a fixed name.

138: The initial directory when browsing for source files and other files (except project files) is no longer stored in the registry. Instead, it defaults to the project directory whenever a project is opened or saved, and changes are subsequently remembered for that session only.

142: When new source files are added, instead of being added at the end of the file list in the Files pane, they are now inserted at the correct positions alphabetically in the list.

145: The option to record error, warning and information message to file instead of to the user interface has been removed. In its place is an option to generate a Verification report.

1262: When saving changes to the Settings pages, the Project Manager didn't warn if a filename or directory is required but none has been provided.

1269: The global build management option to preserve the old time stamp on unchanged header files when generating C++ did not work in version 4.0 or 4.10.

1280: The Project Manager sometimes crashed if it was closed while PDTool is running.

(d) Perfect Developer built-in types and runtime library changes and bug fixes

141: Additional overloads of the findFirst and findLast members have been added to class seq of X.

1225: When the C# library is used, files opened using members of class Environment were always opened in exclusive mode, even when the open mode was read-only.

1240: When serializing and deserializing unions, a union whose actual value was a map could not be round-tripped.

1251, 1284: When the C# library is used, if an attempt is made to open a file containing invalid characters in the path, an uncaught exception of type System.NotSupportedException or System.ArgumentException could be thrown.

1261: When the C# library is used, if a file was opened in append mode using the open member of class Environment, the library method would throw an uncaught exception of type System.ArgumentException.

1274: When the Debug build of either the C++ or the Java runtime library was used, a call to the makeDirectory member of class Environment could terminate with a precondition failure exception.

1278: The C# version of the runtime library did not always correctly process filenames that use the forward slash character as a path component separator.

APPENDIX D: ADDITIONAL CHANGES SINCE PERFECT DEVELOPER VERSION 4.0

(a) New language features and bug fixes

121: Perfect now supports class history invariants, with the option to exempt certain schemas from having to obey them. A new keyword exempt has been added, so this word may no longer be used as an identifier. For details of how to use history invariants, see section 7.1.11 of the Language Reference Manual.

131: Perfect now supports properties with postconditions. This provides a convenient way of describing expected consequences of calling schemas, especially where multiple variables are modified. See section 6.9 of the Language Reference Manual for details.

1218: It was not possible to define operator ~~ recursively because the grammar did not permit a recursion variant.

(b) New compiler/verifier features

117: When a proof fails, if a suggestion is available in the unproven output file then this is now mentioned in the warning message.

123: When warning about a recursive call with no variant, the location of the call target is now given. This is the location of the function, schema, selector, operator or constructor where the variant needs to be added, which may be a function, schema, selector or operator that is overridden by the current one.

132: Code generation in smaller subsets of C++ ("Embedded C++") and Ada ("SPARK Ada") is now supported, making it easier to avoid dynamic memory allocation in the generated code. There are restrictions on unrefined constructs that may be used in Perfect source when generating code in these languages. [NOTE: code generation for these new output languages, as well as for full Ada, is not complete in this release; neither is library support for any of them provided.]

133: When Ada or SPARK Ada is selected as the output language, preconditions and postassertions are translated to the corresponding SPARK annotations. [NOTE: this feature is incomplete in this release, in particular for preconditions and postassertions containing 'for..yield', 'those', 'that' and 'any' expressions.]

(c) New Project Manager features

119: When the Quiet Level is set to Noisy in the Project Settings, the command lines used to invoke the compiler/verifier and other external tools are displayed.

134: Postconditions of the form "change x, y satisfy ?" are now supported.

(d) Compiler/verifier bug fixes and improvements

In addition to the following, numerous corrections have been made to the Ada code generation.

821: One of the tests for integer overflow in the prover made the rewriter loop.

1006: Under rare conditions involving type renamings and redeclarations, the compiler would terminate during the type name binding phase if just a subset of the files in the project were being compiled or verified.

1109: Integer overflow could occur in the prover when negating the most negative integer.

1115: Arithmetic overflow could occur during rule generation from terms involving very large integers, possibly leading to invalid rules.

1148: Where a type has conditional fields, generated code should preferably compare any fields referred to in the guards before comparing the guarded fields.

1159: If the collection operand of 'those' or 'for..those' can be expanded, then the rules used by the prover to normalize the elements may be branchwise incompatible with each other, causing the prover to terminate with a diagnostic if proof output is enabled.

1160 (critical): When the prover applies rule "expand literal 'those'" or "expand literal 'for..those'", when it simplifies the predicate applied to the elements of the collection, it discards the branch dependencies of the rules used unless proof output is enabled.

1167: When generating unification rewrites the prover would only use the first one. This could result in proofs failing under PD 4.0 where they succeeded under PD 3.x.

1168: If the user tries to build or check just some files in a project, and one of the final classes in those files contains an invariant that calls a non-early function declared in one of the other files, then the compiler may crash in the analysis phase.

1170, 1171: The code generator could terminate if Ada code generation was attempted.

1174: The default target compiler when generating C++ code is now ISO instead of Microsoft. The ISO setting is suitable for most modern C++ compilers, including Microsoft VC++ 2005 and 2008, and gcc 4.3.

1175: If the operand of an over-expression is a function call, then in the generated code the function should be called only once, for efficiency. In practice it is called 2n+1 times, where n is the number of elements returned by the function.

1177: Intermediate internal invariant checks were not generated for an if-statement.

1178: Intermediate internal invariant checks were not generated for the invariant, variant and until-parts of a loop statement.

1180 (critical): The verification conditions generated for the second and subsequent guarded expressions of an opaque conditional expression were incorrect, because the verification condition generator assumed that previous guards are false as if the conditional was not opaque.

1182: In rare circumstances a pair of incompatible eliminations could be generated, leading to a circular rewrite and prover termination with a diagnostic.

1184: The prover would sometimes greatly exceed the time limit or memory limit when attempting paramodulation.

1187: Direct recursion in a function, schema or constructor is now an error, not a warning.

1192: If a parameter was declared with type is A || B where B was a constrained type, then when calling the function with actual parameter "e" we generated a verification condition "(e within B) ==> p(e is B)" where p(x) is the constraint of B. However, we should instead generate "(e within C) ==> p(e is C)", where C is type B with the constraint removed.

1199: If an expression of the form x! / e or x! % e with integer x and e was used then the generated code failed to compile.

1200: In the expression (e after it!s), if s is a non-early schema then the prover should have assumed that the whole class invariant holds for the expression, but did not. This could lead to failed proofs, especially if the schema definition was not available.

1201: The prover would terminate abnormally when completing a proof if the final confirmed term depended on an uninstantiated metavariable.

1203 (critical): When accessing a guarded data member of a class object, verification conditions that the object can be evaluated were discarded. This matters when accessing a guarded data member of an object returned by a function call, for example.

1205: When generating a cross-reference listing, the compiler always removed any existing extension in the specified output filename and substituted ".xref".

1209: The prover sometimes failed to unify terms, in particular when a numeric metavariable occurred in more than one operand of an expression and the required substitution was of the form x + c where c is a literal.

1211: Occasionally the prover will complete the proof of a branch but fail to recognize that it has done so and report that the verification condition is unprovable.

1212: If proof output is enabled, occasionally PDTool will fail to reconstruct the proof trace, leading to incomplete proof output and a warning message "reconstructed proof output is incomplete".

1213 (critical): When using nested quantifiers, under rare conditions an in-bounds term from an outer quantifier was used to rewrite an expression inside an inner quantifier, and the result of the rewrite contained the outer bound variable. In such cases an incorrect rewrite was done, typically leading to a proof failure.

1216: A minor prover performance issue has been corrected.

1217: The proof of transitivity of a user-defined ~~ operator timed out in a fairly simple example.

1219: When a schema postcondition of the form "A then B" conditionally changed one element of a sequence or mapping in part A and another in part B, some information about the unchanged elements could be lost, leading to failed proofs.

1221: When command line options were factored, spaces embedded in the option strings were removed.

(e) Project Manager bug fixes and improvements

1156: The close button did not work on the Settings dialog or Cross-Reference dialog.

1162: When the project path included components containing spaces, and the default browser was FireFox, then the "Go to proof information" option on the menu displayed after right-clicking on an error, warning or information message did not work.

1163: On some systems the cross-reference dialogue did not start PDTool when the Go button was pressed, and no cross-reference was generated.

1173: When no project is open or a build, check or verify operation is in progress, the configuration selection in the toolbar should be disabled.

1193: Clicking on the close-box at the top right corner of the Configurations dialog window did nothing.

1194: If a user created a new configuration and then pressed the Close button in the configurations dialog, it opened the Settings notebook for the original configuration, which was confusing.

1195, 1196: The input box for the namespace/package name on the Code Generation page of the Settings notebook was sometimes incorrectly enabled or disabled.

1202: Under Windows Vista, when the Stop button was used a spurious "Failed to kill process" popup message appeared.

1204: When the compiler generated an error or warning message that included the text "see [...]" where ... is a location, the popup menu when the message is right-clicked did not include an option to go to the referenced location.

1206: In the cross-reference listing, constructors were grouped together and ordered by location of their declarations. They are now ordered first by class name.

1207: When generating a cross-reference listing, if the setting of the "Unreferenced declarations only" box was changed then the project manager flagged the project as having changed.

1214: When creating a new file, the default author text is "Automatically generated by Perfect Developer". This is confusing because it suggests that the file was produced by a code generator.

1222: Options specified in the Additional Options field of the Miscellaneous tab in the Settings notebook were sometimes duplicated when generating the PDTool command line.

(f) Library bug fixes and improvements

1161: (C# only) When deserializing a storable class, if the data was not valid then the .NET Framework deserialization library could throw various exceptions other than the ones documented, and these additional exceptions were not caught by the Perfect library.

1164: (C# only) The return value for Environment caseSensitiveFileNames was always true even on Windows systems.

1166: (C# only) If toString is called on a real having a small integral value then it it printed in integer format, without the trailing ".0".

1172: Set union was sometimes very slow when uniting a small set and a large set.

1197: The stdin, stdout and stderr streams were not represented in the Environment state variables, and the members that read and write these streams were left undefined. This made it difficult to specify and refine operations involving e.g. writing to stdout. Note that the Environment member functions stdIn, stdOut and stdErr no longer guarantee to return open streams, because it is possible to close these streams prior to invoking the program.

1198: The integer abs member function was missing from the libraries.

1208: The C# library now implements the getImageVersion members of class Environment. The moduleName parameter (if not empty) is assumed to be the base name of an assembly.

1120: File Throw.hpp (which is included by Ertsys.hpp) was not included in the Windows install.

(g) Documentation corrections and improvements

In addition to the following, various minor improvements have been made, and new features documented.

941: The Language Reference did not describe how to construct a main program in Perfect.

1190: The Language Reference did not state that any postassertion must refer to at least one modified variable or to the function result.

1210: The User Guide stated that the default error reporting level was 3 when in reality it is 2. 

Escher Technologies Limited, 22 February 2013.