README file for Escher Verification Studio version 7.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.0

0. VERSION IDENTIFICATION

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

	VerificationStudio executable	7.0
	EscherTool executable		7.0
	builtin.pdc			7.00.00.00
	ecv.pdc				7.00.00.00
	rubric.pdc			7.00.00.00
	Documentation files		7.0 and 7.01

The only changes between release 7.0 and 7.01 are to the Escher C Verifier documentation.

1. PLATFORM REQUIREMENTS

Escher Verification Studio is intended to be installed on a PC with a 1GHz or faster processor, at least 4Gb of memory, and a 64-bit Windows 7, Windows 10 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 already have Escher Verification Studio 6 installed, you can leave it installed on your computer if you wish. Escher Verification Studio 7 uses a different directory and registry key structure, so the two installations will not interfere with each other.

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 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.
•	queue.cpp demonstrates verification of a C++ templated class.

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

1398 (Escher C++ Verifier only): The semantics of calls to constructors is not fully implemented, so you may encounter verification failures if your C++ program contains constructor calls.

(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, this does not work in all browsers, in particular some versions of Internet Explorer. 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.0

(a) Changed behaviour

Escher Verification Studio is now built as a 64-bit application, requiring a 64-bit operating system. Operation under Windows XP and Windows Vista is no longer supported.

159: (eCv only): 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

(PD only): Perfect Developer now includes a new code generation language "ADA (SPARK)" which generates annotations compatible with SPARK 2014 and later.

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

(eCv only): eCv now supports local assume-statements.

153, 154 (eCv only): eCv now supports a wider range of C++ constructs. 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.

165 (eCv only): eCv now supports the "#warning" preprocessor directive, which is a common extension supported by many C and C++ compilers.

166: In the Project Manager, you can now build, check or verify a file that is open in the editor by right-clicking on the tab and selecting the corresponding entry on the popup menu.

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.

(c) EscherTool bug fixes

1344 (eCv only): 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 optimized 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.

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.

1401 (eCv only): When the heap in a parameter list is rewritten, the text "<placeholder>" may appear in the proof output.

1405 (eCv only): The mechanism to determine the conditions under which writing through a pointer is permitted doesn't allow for writing through pointers to local variables. This leads to spurious error messages of the form "Assignment to expression ... of type ... is not permitted by the writes-clause of function ...".

1406 (PD only): If a trace expression has an operand that contains a binding error, then the compiler hits an internal breakpoint that reports "Internal error: binding failed for expression: ###.toString" where ### is an expression containing the binding error, and doesn't report the actual binding error.

1411 (eCv only): If a nonstatic data member of integral type is declared in a class and the bounds of another member of array type refer to this data member (which is not legal C++), then eCv hits a breakpoint, causing termination.

1413 (PD only): In certain situations, the prover failed to perform a necessary type substitution when generating semantic information for an 'after' expression with templated types, resulting in failure to find a proof,

1414 (eCv ony): Binary literals were interpreted incorrectly.

1415 (eCv only): eCv did not allow a C-cast or a static_cast to a type defined by a constrained typedef.

1417 (eCv only): The C++ build of eCv crashed when the input file contained a Unicode ellipses character. 

1418 (eCv only): When a value is assigned to a bit field, VCs should be generated to ensure that the value being assigned fits in the bit field. The correct VCs were generated for unsigned bit field types, however for signed bit field types the range of the bit field was taken to be the range of an int, without regard to the number of bits.

1419 (eCv only): If a macro expanded to an expression involving a ## b ## c then the second ## was not processed.

1420 (eCv only): If the same identifier was used as the name of more than one argument in a macro definition, no diagnortic was given.

1421 (eCv only): MISRA-C 2012 explicitly allows the type of a bit field to be a typedef that is a synonym for an allowed type; bit eCv allowed 'signed int' and 'unsigned int' only.

1422 (eCv only): We have an example from a customer that gave rise to a non-terminating rewrite in the maths engine.

1423 (eCv only): The prover sometimes failed to make use of a global assume-statement in constructing a proof, if the assume-statement included a function call.

1424 (eCv only): eCv required every postcondition to refer to 'result' or a modifiable non-local entity. This meant that a postcondition such as "post(true)" could result in a message saying that the postcondition must refer to 'result', even for a function returning void.

1425 (eCv only): If a typedef-declaration defined a name for as array type, and that name was subsequently used as the type of a parameter in a function declaration, then the parameter type was incorrectly treated as an array instead of a pointer, leading to various error messages or verification failures.

1426 (eCv only): If a variable was written in a loop body only when the code was about to break, the instancing of that variable after the loop was incorrect, leading to verification failures.

1427 (eCv only): eCv incorrectly allowed a ghost variable to be assigned in a non-ghost statement. This would cause a problem when compiling the code, because the compiler would be unaware of the ghost variable.

1428 (eCv only): eCv allowed a ghost statement to change the values of non-ghost variables.

1429 (eCv only): eCv did not allow side effects in initializers for local variables.

1430 (eCv only): eCv did not treat a variable declared in a ghost statement as a ghost variable.

1431 (eCv only): Local assume-statements sometimes didn't make a proof possible when they should have done so because of incorrect instancing.

1433 (eCv only): Using the unary & operator to take the address of a local variable whose type was declared using a constrained typedef yielded type pointer-to-unconstrained-type instead of pointer-to-constrained-type.

1434 (eCv beta version 6.10.05 only): EscherTool terminated abnormally when a C source file contained a call to an undeclared function.

1435: The verifier was sometimes unable to prove that the value of a conditional expression conformed to a type constraint because it had discarded relevant givens.

1436: The verifier sometimes produced incorrect results when attempting to prove verification conditions that involved the 'rep' operator on a bag, especially if all the elements in the bag were literals.

(d) 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.

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.

1397: If several files were open in the editor, and the order of the tabbed pages was changed by dragging tabs, then the right-click menus on tabs that changed position might be incorrect.

1402: When the Find Definitions function of the editor was used on a C or C++ file, it didn't look for definitions of the identifier as a macro.

1407: If a source file contained certain characters e.g. 0x91 or 0x92 (left and right single quotes in Windows code page 1252), then when the editor loaded the file, those characters were not displayed; and when you tried to save the file, it silently wrote an empty file instead.

1410: File...Save As now clears annotations in the current file window, because they no longer relate to the file in the window.

(e) 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 language standard header files, for use with C++ source code.

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

1408 (eCv only): Files stdint.h and cstdint were not included in the standard library header files supplied with eCv. These files are required by C99 and C++ 2011.

1409 (eCv only): The precondition of strcpy was incorrect. It required the destination array to be 1 character longer than was actually necessary.

1416 (PD only): The C++ build of the runtime library returned true when isDigit() is called on certain extended characters, for example the ellipses character.

Escher Technologies Limited, 26 April 2017.