================================================================================
$Header: /home/rda/opp/RCS/CHANGES,v 1.142 2007/11/22 16:29:35 rda Exp $

ProofPower Changes History
================================================================================
2.7.8

PPTex:

1) The scripts doctex, docdvi, etc. will now accept any legal file name
(previously file names containing spaces were not processed properly).

PPHol:

1) The scripts pp, pp_list etc. will now accept any legal file name (previously
file names containing spaces were not processed properly).  The commands with
-i or -f options no longer accept comma-separated lists of file names, so that
file names may contain commas. A list of -i or -f options may be used to
achieve the effect of a single option with a list of file names.

2) A new function for constructing term orderings, make_term_order, has been
provided, which is much more powerful and easier to use than the old function
gen_term_order (which is retained for backwards compatibility). The repertoire
of functions for constructing orderings on ML types has been extended and moved
into a separate structure Order with its own section (2.10) in the reference
manual USR029. These facilities have been used to reimplement the term ordering
for the real numbers which fixes a number of problems with %R%_term_order.

This change may affect some proofs involving real numbers, since the change
affects the arithmetic normal form produced by %R%_anf_conv, but this is
expected to be quite rare (the ProofPower mathematical case studies only needed
1 small change).

3) A quantifier elimination procedure for real linear arithmetic is now
provided as a conversion %R$_lin_qep_conv. There are also a number of new
conversions and conversionals that are useful in implementing quantifier
elimination procedures (see USR029 section 8.7).

PPZed:

1) The scripts zed and zed_list have been changed to accept any legal file name
(see change (1) to PPHol above for details).

2) Functions mk_dollar_quoted_string and dest_dollar_quoted_string have been
provided to assist in programming applications that use the quoted identifier
syntax ($"..."). The implementation of quoted identifiers has been made more
robust. Quoted identifiers are no longer allowed as parts of fancyfix
identifiers.

3) ML names that refer to the integer range operator now uniformly refer to it
as dot_dot. The conversion formerly known as z_dots_conv is now called
z_simple_dot_dot_conv.

PPDaz:

1) Z quoted identifiers may now be used in pre- and post-conditions.

2) There is now a function delete_deferred_subprogram that allows
the development steps for a deferred subprogram to be undone.

================================================================================
2.7.7

PPDev:

1) The SLRP parser driver function slrp'parse now only calls the lexical
classifier function once for each token read.

2) The support for automatic generation of the reduction functions in SLRP has
been made more flexible. The command line interface has new options -b and -r
which make it easier to build a parser by mutating  the automatically generated
reduction functions.

PPXpp:

1) Symbols for set symmetric difference, sequence extraction and functional
composition in the ISO standard Z toolkit have been included in the fonts.

2) The file selection dialogue now retains its state if there is a problem
accessing the file rather than just cancelling the operation (so that you can
choose whether to fix the problem or to cancel the operation).

3) Dismissing an error dialogue using the ESC key now works properly for
all dialogues.

4) The Goto Line operation now selects and highlights the line you have
jumped to.

5) When you open a read-only file, xpp no longer prompts for confirmation
(unless you are working as super-user).

6) When you attempt to quit, xpp no longer checks whether the application
is running.

PPTex:

1) The symbols for set symmetric difference, sequence extraction and
functional composition in the ISO standard Z toolkit are now supported.
The ASCII keywords reflect the ISO standard in using %fcomp% for
functional (right-to-left) composition and %rcomp% for relational
(left-to-right) composition. The keyword %fcompose% formerly used
for relational composition has been withdrawn.

2) Underscore characters are no longer allowed in multi-character subscript
or superscript strings introduced by the %down% or %up% characters.

PPHol:

1) There is a new tactic intro_%forall%_tac1: intro_%forall%_tac1 x
being equivalent to the common idiom intro_%forall%_tac(x, x).

2) Names that were previously prefixed with "icl'" to indicate that
they are not for normal use are now prefixed with "pp'".

3) The signature of the logical kernel has been rationalised and the standard
kernel interface has been made more efficient. Apart from minor changes to
error messages, this change should be invisible in all normal use of the system
using the standard functions to access the logical kernel such as new_theory,
new_parent etc. There is now a function kernel_interface_diagnostics that can
be used to resolve problems caused by use of internal functions such as
pp'new_theory, pp'new_parent, etc.

4) The functions get_const_theory and get_type_arity have been moved from
the structure SymbolTable to the structure KernelInterface. This allows
a more logical and more efficient implementation. This change is only visible
to users doing very low level programming of the system.

5) Some extra theorems about finiteness and the size of finite sets have
been added to the theory fin_set. The theorem %union%_finite_thm has
been changed from an implication to a more useful bi-implication.

6) save_thm, new_conjecture and related functions now enforce the convention
that, if a theory contains a conjecture and a theorem stored under the same key,
then the theorem must prove the conjecture. This convention has been used to
provide new functions is_proved_conjecture, get_proved_conjectures and
get_unproved_conjectures.

7) The theory of real numbers now provides exponentiation for integer as
well as natural number exponents. Note that this overloads the symbol "^"
so you may need to add a type constraint to resolve the overloading.

8) The files specified in the `-i' option to pp are now processed after
calling any functions registered with new_init_fun.

9) The proof context '%bbR% now includes %bbR%_frac_norm_conv in its rewriting
conversions. This means, for example, that it will now automatically rewrite
2/4 to 1/2.

10) The function force_get_cache_theory now creates a new cache theory rather
than using the current theory if none of the existing cache theories is usable.

11) The script pp(1) now has a -q flag to suppress subgoal package output in a
batch run of ProofPower. This is complementary to the -v flag which now forces
subgoal package output.

12) By default, non-ASCII characters in HOL character and string literals are
now pretty-printed using the extended character set rather than using ML escape
sequences.  ML escape sequences are used if the flag pp_use_extended_chars is
false.

13) The ML types TYPE and TERM are now equality types. The functions "=$" and
"=:" have been retained for backwards compatibility, but ordinary ML equality
may now be used to compare TYPEs and TERMs. ("~=$" must of course still be used
to test for alpha-equivalence).

14) Floating point literals are now supported (see USR005, ProofPower
Description, for the syntax).

15) The theory of sets now includes the symmetric difference operator (using
the same symbol as in Z).

16) Functions Max%down%R and Min%down%R that give maxima and minima of lists
are now supplied in the theory of real numbers along with supporting
conversions etc.

PPZed:

1) The theory of sets in the Z library now provides the symmetric difference
operation in line with the ISO standard Z toolkit. All proof contexts that
previously contained rules for handling union, intersection and set difference
now include analogous rules for symmetric difference.

2) The theory of sequences is now in line with the ISO standard Z toolkit.
I.e., the squash operation that converts a finite partial function into a
sequence is defined and used in the new definition of the extraction operator
and in the revised definition of the filtering operator.

3) Names that were previously prefixed with "icl'" to indicate that
they are not for normal use are now prefixed with "pp'".

4) The syntax for let-expressions now uses ";" rather than "," to separate
the definitions (which brings the syntax closer to the ISO standard). A bug
in the processing of let-expressions has also been fixed.

5) Decorated fancyfix identifiers are now supported. E.g., if _ op _
is declared as an infix operator, you can use _ op _ as a signature
variable in a schema, and decorating the schema will produce schemas
with signature variables such as  _ op' _, _ op! _, _ op? _, etc.

6) "Decor" or "decor" is now used systematically as the abbreviation
for "decoration" in names such as is_decor%down%s (which was previously
called is_dec%down%s).

7) The Z lexical rules have been extended to allow a Z identifier to
be given as a `$` immediately followed by a string quotation. This
makes it possible to embed a complex namespace in the Z namespace without
having to encode names as alphanumeric strings.

8) The new symbol for functional composition is now used in the Z library
rather than an ASCII 'o'.

9) Floating point literals are now supported (see USR005, ProofPower
Description, for the syntax).

10) The proof context 'z_reals now includes z_%bbR%_lit in its rewriting
conversions. This means that it will now automatically normalise fractions
made up of numeric literals.

11) The change to force_get_cache_theory in PPHol (see above) means that when
Z terms are parsed, a new cache theory may be created, if necessary, to hold
any supporting HOL definitions (previously, the current theory was used as
the cache theory, if no other cache theory was available).

12) By default, non-ASCII characters in Z character literals are now
pretty-printed using the extended character set rather than using ML escape
sequences. ML escape sequences are used if the flag pp_use_extended_chars is
false.

13) The coverage of the conversion z_let_conv has been extended.

14) Several problems with type-checking of let-expressions have been fixed.

15) The bag bracket symbols are now treated as punctuation (or "stops" in the
terminology of USR005, ProofPower Description).

16) There is a new conversion z_dot_dot_conv which expands ranges with
signed integer constant bounds, into set displays, e.g., ~1 .. 1 = {~1, 0, 1}.

PPDaz:

1) A new keyword $IMPLICIT is supported that enables the user to declare
subprograms that are implicitly declared in Ada. This is for use in package
bodies when subprograms declared in the package specification are used
before the subprogram body has been introduced.

2) The functions fmt_exp and fmt_exp1 in the CNAdaOutput structure are
now made visible for use by implementors of extensions to the system.

3) Aggregates inside other aggregates are no longer required to occur
inside a qualified expression.

4) Names that were previously prefixed with "icl'" to indicate that
they are not for normal use are now prefixed with "pp'".

5) Unions arising from translating array aggregates now respect the
left-associativity of the union operator.

6) Some bug fixes, performance enhancements and enhancements to the error
handling have been implemented.

7) `$' characters may now be used in the Z parts of a Compliance Notation
script.

8) The definitions in the theory 'cn' have changed to accommodate the change to
the name of the functional composition operator in the Z library.

9) The mapping of the Ada namespace into Z has been adjusted so that a single
theory can be used to represent the contents of a package specification both
for the package body and for program units that refer to the package. This
means that the Z translation of the types, constants and variables declared in
a package specification is now the expanded name, i.e., it includes the package
name prefix.  Program units that refer to subprograms in the package do so
using the expanded names, whereas inside the package body the simple name is
used.

10) The names used for a Compliance Notation script must now be derived from
the name of the Ada compilation unit it contains. See USR504: Compliance
Notation Language Description section 3.5 Program Structure for details of
the naming conventions.

11) The names of Ada entities in Z expressions must now be given in their
canonical expanded form. This means that the names of types, constants and
variables that are declared in a package specification must now be referred
to with the package name prefix in all contexts. If you do use the form
without the required prefix, the error message will tell you what the
canonical name is.

12) Expanded names involving package names, subprogram names, block names
and loop names are now fully supported - any valid Ada name for an entity
may be used in the Ada parts of a script.

13) Z floating point literals are now used in the translation of Ada real
literal expressions.

14) Renaming definitions for functions and constants no longer give rise to
abbreviation definitions. Note that this means that pre- and post-conditions
must now refer to the renamed function or constant using its original name.

15) Every subprogram body and block is now associated with a theory to hold the
Z paragraphs arising from its declarative part and its sequence of statements.
This is the script theory for a subprogram body appearing as a compilation unit
and is an automatically generated theory for subprogramms and blocks appearing
in packages or other subprograms.  See section 3.5 of USR504, Compliance
Notation Language Description for more information. 

16) A function get_script_theories is provided to list all the theories
associated with a Compliance Notation script.

17) The name of the type in a use type clause may now be given as an
expanded name (i.e., prefixed with a package or subprogram name).

18) A string control cn_spark_annotation_char is now provided to control the
character that distinguishes SPARK annotations from other Ada comments.

19) The string control "case_of_ada_keywords" has been renamed as
"cn_case_of_ada_keywords" for uniformity with other control names.

20) The new command open_scope has been provided to navigage into
the scope of a nested subprogram.

21) It is now possible to defer the generation of Z for a nested
subprogram using a new keyword $deferred. This makes it possible
to give the formal development of the body of a nested subprogram
in a child database.

22) The parametrisation of new_script and related commands has been changed so
that the name and type of the compilation unit are given separately with the
name being given in Ada rather than in its Z translation.

23) Formal parameters may no longer be included in the global dependency
list of a subprogram. When a procedure is called, the global dependencies
of the called procedure must now appear either in the frame of the
specification statement being refined or in the global dependency list
of the calling procedure.

24) A theory is now introduced to represent the scope of a block statement.
The theory is named <block_name>'block, where <block_name> stands for the
expanded name of the block. This makes the treatment of the scope for
block statements uniform with subprograms.

25) The tool now attempts to check whether a range in a real type definition is
empty and reports an error if it is. If it is not possible to check
automatically whether the range is empty, a VC is generated. (Previously
this was only done for integral types).

================================================================================
2.7.6

PPXpp:

1) xpp should now work on recent Linux systems that support the grantpt
method for allocating pseudo-terminals and not the older /dev/ptyXXX method.

2) A bug whereby the Palette and the Templates Tool would sometimes insert
text in the wrong place has been fixed.

3) A bug under Mac OS X which made the Restart Application item in the
Command menu unreliable has been fixed.

4) A problem with the font files on some systems (duplicate/mismatched
FONT properties) has been corrected.

5) A keyboard accelerator (Ctrl+D, by default) is now defined to bring
up the Command Line Tool.

6) When you apply a change to the command line in the options tool, you
now get a dialogue asking if you want to restart the application.

7) The fonts now includes glyphs for blackboard bold B, C, and S.

PPTex:

1) The style and keyword files now support the font characters for
blackboard bold B, C and S.

PPHol:

1) The system initialisation interfaces have been tidied up. This gives
some minor improvements in the behaviour. For example, the function
Initialisation.new_init_fun now provides a general facility for registering
a function to be called at the start of a session.

2) A function on_kernel_inference is provided which lets you register functions
to track applications of the built-in inference rules.

3) The function app has been added to the ML utilities and is used in
a number of places where previously map was used.

4) Left associative operators are now supported in ProofPower-HOL. This
introduces new functions: declare_left_infix, declare_right_infix,
get_left_infixes and get_right_infixes. The function get_infixes is no longer
provided, but declare_infix remains as another name for declare_right_infix.
The datatypes FIXITY and ASSOC used by the parser and pretty-printer have also
been changed to accomodate parsing of left-associative oeprators.

5) Left associative operators are now used in the ProofPower-HOL theories to
make terms involving arithmetic subtraction, set difference and similar
operators associate as one would expect. Following HOL Light, this is done by
making the operators in question left-associative and giving them higher
precedence than the related associative operations (such as addition) which
remain right-associative.

6) A problem with arithmetic normalisation for the reals (%bbR%_anf_conv)
has been fixed, this also fixes some problems the linear arithmetic
decision procedure for the reals (prove_tac in the proof context "'%bbR%").
This may affect proofs involving terms of the form %bbN%%bbR% x or x/y where
x is not a numeric literal (the decision procedure may succeed in proving
goals that it previously could not).

7) The theory of reals now includes the embedding %bbZ%%bbR% of the integers
in the reals and some basic theorems about it.

8) A bug in pp_list that meant it would sometimes update the database if
interrupted has been fixed.

9) There are new functions oe_key_flatten, key_mk_const, key_dest_const,
key_mk_ctype key_dest_ctype, get_const_keys and get_type_keys. These have been
used to increase the performance of some operations with theories (such as
open_theory) when the theories involved contain very large numbers of types
and/or constants.

10) A bug leading to a possible variable capture problem in type instantiation
of terms (inst and rules such as inst_term_rule that use it) has been fixed.

PPZed:

1) The precedence and associativity of infix operators in the Z library
is now in line with the ISO Z toolkit.

2) The syntax for fixity paragraphs now allows the templates to be
enclosed in brackets (as required by the ISO standard syntax).

3) A handful of new theorems about finite cardinalities has been
added to the theory z_numbers1.

4) Schema projection is now a right-associative operator and no
longer fails in the (not very useful) case when the signature
of the second operand subsumes the signature of the first operand.

5) In a schema quantification, the schema text operand may now declare
variables that are not in the signature of the schema operand. This brings
this language feature in line with the intentions of the ISO Z standard.

6) The theorems z_dom_clauses and z_ran_clauses used only to apply to relations
whose domain and range have the same types. This restriction has been relaxed.
This makes the theorems and several proof contexts that use them more powerful.

7) Various restrictions on the operands of schema composition have been lifted.
Any combination of operands for which the defining property of schema
composition is well-typed is now allowed. This brings this language feature
in line with the ISO Z standard.

8) Let-expressions are now supported (see usr005.dvi for the syntax).
Conversions z_let_conv and z_let_conv1 are provided for reasoning
about let-expressions.

9) The global variables BOOL and CHAR have been renamed as blackboard
bold B and S (for "symbol" or "schriftzeichen").

10) The HOL types corresponding to given sets or free types in Z now
have their names decorated with a leading "z'".

11) The syntax for operator templates has been extended to allow
the Z standard from ",," as a synonym for "..." and to support
two new forms of stub: "_?" and "_!" which make higher-order
operators (i.e., operators whose operands can range over predicates)
easier to use. The Pi operator is now defined using "_?".

12) Conditional expressions and predicates are now supported (the
conditional is defined as a higher-order operator "if _? then _! else _!"
in the theory z_sets). The main proof contexts for Z will simplify
conditional expressions whose condition is given as "true" or "false".

13) A dollar character followed by a string quotation may now be used in Z in
much the same way as in HOL, to form a variable name whose syntax need not
conform with the lexical rules. Unlike HOL, no space is allowed after the
dollar character, so the dollar character can still be used to form ordinary
Z identifiers.

14) There is a new inference rule rule z_gen_pred_u_elim which can
simplify working with the definitions of generic global variables.

15) The schema operators that have the same names as logical connectives
(i.e., the three sorts of quantification, conjunction, disjunction,
implication and bi-implication) now have alternate names with a subscript
"s" (by analogy with the other schema operators like composition). This
can make complex expressions involving both logical and schema operators
easier to read. A flag subscript_z_schema_operators is provided, defaulting
to false. If the flag is true, the parser will not accept the unsubscripted
forms of the name as schema operators.

PPDaz:

1) Labelled statements are now supported (the label is ignored in the
formal treatment). This allows formal development of code containing
labels, but not goto statements, e.g., for documentary purposes.

2) Goto statements are supported informally.

3) VC generation now keeps a closer track of where in a sequence of
statements variables may change. This causes provable VCs to be
produced in several cases where correct code could not previously be
verified.

4) There has been a minor improvement to the generation of domain
conditions in VCs arising from for-loops with variable bounds.

5) The syntax of the Compliance Notation has been changed so that
keywords must be prefixed with a dollar sign.

6) A function create_package_spec_theory is provided which lets you
create the package specification theory before introducing compilation
units that refer to the package.

7) Derived types are now supported.

8) When generation of domain condition is enabled, domain conditions
are now produced asserting the type or subtype constraints that apply to: (i),
actual parameters of mode in or in out in a procedure call; (ii), the
right-hand sides of assignment statements; and, (iii) the returned
expression in return statements in function bodies.

9) The not and array_not operators in the theory cn now have precedence
50 (the same as "**" following the rules for the Ada operators).

10) Informal development steps now result in warnings. E.g., a warning
is produced if a specification statement is given for a subprogram
in a package specification but no specification statement is given
for it in the package body.

================================================================================
2.7.5

PPXpp:

1) The palette tool now avoids a problem with sprintf on some systems that
caused the buttons to be labelled with hex digits rather than mathematical
symbols.

2) Some default values in the example resource files have changed (width of
file name text field is now 24, maximum size of journal is now 1,000,000).

3) A number of minor changes have been made to the dialogue boxes, particularly
ones with text windows to make their behaviour more uniform.

4) Several minor bugs have been fixed, e.g., earlier releases gave
an incorrect warning that the file had been changed under some conditions.

5) If you try to open a binary file, the dialogue warning you that this
has drawbacks gives you the option not to continue.

6) The supplied example applications defaults files suppress the unintuitive
behaviour of the Home and End keys in file selection dialogues.

7) The file selection dialogues now reset the file name field whenever they
are popped up.

PPHol:

1) The theory fin_set now provides theorems giving the basic facts about sizes
of finite sets along the lines of those provided for ProofPower-Z.

2) File names with the letter `Q' in them are now supported properly
by use_file and the theory listers.

PPDaz:

1) It no longer causes an error to process a renaming declaration for a
informal subprogram.

2) It is no longer permitted to have an informal procedure and a formal
procedure of the same name. This fixes a potential unsoundness.

3) A flag cn_ignore_spark_annotations has been introduced which causes
Ada comments of the same form as SPARK annotations to be ignored.

4) Forward declarations of informal functions are now supported.

5) The Z paragraph that represents a function renaming in a package
specification is now an abbreviation definition (making this case
uniform with other places where function renaming occurs).

6) The force of use clauses in package specifications now propagate into the
package body.

================================================================================
2.7.4

General:

A file VERSION is now included in the ProofPower home directory identifying
the version of the system.

PPXpp:

1) The Search and Replace tool has been simplified: the rarely used buttons for
"search-then-replace" have been removed as have the ":= Selection" and "Empty"
buttons (the functionality of the latter two is available by right-clicking in
the text areas); the toggle buttons that control the options "ignore case" and
"use wildcards" (previously known as "use regular expressions") are now in the
Search and Replace tool window and so the "Options" button is no longer
necessary.

2) The execute function in the Command Line tool now reports back to you
if the application is not running.

3) A bug in the (non-wildcard) search function has been fixed.

4) A bug in the command-line option processing on Mac OS X and Solaris
has been fixed.

5) The file selection dialogues now reread the contents of the directory
whenever they are popped up.

6) The keyboard accelerators (e.g., Ctrl-X for Execute Selection) now
work when the CAPS lock or other shift keys are pressed. N.b., you will
need to update your Xpp resource file (~/app-defaults/Xpp) for these
features to work.

7) The appearance of several of the dialogue windows has been improved.

8) The layout of the palette tool is now user-configurable.

PPHol:

1) The functions list_e_enter and e_stats have been added to
the Standard ML utilities.

2) Type inference contexts are now implemented internally as efficient
dictionaries rather than association lists. The old interfaces for setting and
getting the context as lists are still supported but are supplemented by more
efficient interfaces that give access to the efficient dictionaries.

3) The handling of HOL aliases has been moved into the HOL pretty-printer
rather than the generic pretty-printer (this avoids a sometimes slow
computation with data types when other languages such as Z are pretty-printed).

PPZed:

1) Bracket elimination in the pretty-printing of binding and tuple
selection has been improved (a fix in 2.7.3 was causing unnecessary
brackets to be added).

2) A bug in the pretty-printing of theta-expressions has been fixed.

3) A function z_print_fixity is provided to print out information about
fancy-fix operator symbols (infix, postfix etc.).

PPDaz:

1) The internal representations of the data structures that represent
the Compliance Notation name-space have been radically revised in
the interests of performance and to make them more uniform.

2) It is now legal to repeat a use clauses for a package.

3) The treatment of forward declarations of subprograms is more liberal.

4) The pretty-printing of a package with an empty private part has been
corrected (and this construct will give a non-SPARK warning if those warnings
are requested).

5) Subject to the constraint that they must appear at the top level of a
package body, using declarations are now treated syntactically just like other
forms of declarations and may appear in the expansion of k-slots and may be
freely interleaved with other declarations.

6) The declarative force of some constructs was not previously propagated into
k-slots and specification statements in the scope of those constructs. These
constructs are now propagated in the same way as ordinary declarations. This
applies to use clauses, renames clauses and using declarations.

7) Various bugs have been fixed.

================================================================================
2.7.3

General:

The installation directory has been reorganised so that ProofPower database are
kept in a new directory $PPHOME/db and other non-executable files that were
formerly in $PPHOME/bin are now in a new directory $PPHOME/etc.

It is no longer necessary to set up any environment variables (other than
the search path) for basic use of ProofPower - the executables can now
automatically locate the installation directory and pass its name
to any programs that need it (e.g., the environment variable TEXINPUTS
is automatically set up by texdvi when it runs LaTeX). See the
README file for more details.

The information in the README files for the individual packages that
is still relevant has been moved into a single README file and the original
per-package README files have been withdrawn. The README file has been
reorganised to give a quick summary of what you need and what you do to
carry out a simple installation followed by a more structured description
of how to customize the installation to your needs.

The installation is no longer dependent on the transfig software (the PostScript
files it generates are pre-built when the Open Source packages are made). The
original fig sources are still supplied for developers.

PPXpp:

1) Various minor bugs and user interface glitches have been fixed.

2) xpp will now automatically load the ProofPower fonts for you, there is no
need to call xset in an X initialisation script.

3) The resource Xpp.addNewLineMode in the example resource
file has been changed to default to automatically add new-lines.

4) The xpp command line is now more closely integrated with the command
being run. A command to run by default can now be specified so
that, for example, "xpp -d database" will start an xpp session running pp
on the indicated database.

5) The Search-and-Replace tool has been redesigned: it is now two separate
tools, one for search-and-replace and one for navigating by line number.

6) The organisation of the menus has been changed to be more like other
editors and word-processors, e.g., the Edit menu is now immediately to
the right of the File menu and the Search-and-Replace tool is now started
from the Edit menu.

PPTex:

1) The findfile program now has an option for finding out the real
name of a file or directory specified using a symbolic link. This
is used in the various shell scripts in the PPTex and PPHol packages
to locate the ProofPower installation directory if the user has
not specified it using the environment variable PPHOME.

2) texdvi has a "-b" option which makes it run BiBTeX after running
LaTeX.

PPHol:

1) The theory of finite sets is now equipped with some basic theorems including
a principle of induction and with an induction tactic.

2) The shell scripts all use findfile to locate the ProofPower installation
directory if it has not been specified using the environment variable PPHOME.

PPZed:

1) The name of the generic universal set has been changed from "U"
to a blackboard bold "U" (%bbU%). This means that the only alphanumeric
names defined in the Z library are the ones such as "seq" 
defined in the standard Z toolkit.

2) A bug in the treatment of free variables with decoration by the
type checker has been fixed.

3) The pretty-printer now brackets expressions of the form "x op y op z"
where "op" is a right associative infix operator properly.

4) The fixity definition for sequence concatenation is now in the theory
z_sequences where it belongs.

PPDaz:

1) A number of bugs have been fixed and several error messages improved.

2) The SPARK program is now referred to as the Ada program throughout the documentation.
print_spark_program1 and output_spark_program have effectively been renamed as
print_ada_program and output_ada_program and the old print_spark_program and
output_spark_program have been withdrawn.

3) The name at the end of a package declaration or a proper body is now optional.

4) The private part of a package is now allowed to be empty.

================================================================================
2.7.2:

PPTex:

1) The superscript and subscript shift characters (%up% and %down%) are
now defined to superscript a following alphanumeric identifier or
multi-digit decimal number rather than just the immediately following
character.

2) It is now possible to define a percent keyword to be typeset using
a TeX command that takes as its argument the text following the keyword
matching or delimited by a regular expression.

PPXpp:

1) There are now items "New Editor Session" and "New Command Session" in
the Tools menu which start up new xpp sessions.

2) If either the command to run or the file name is specified on the
xpp command line as an empty string, xpp starts up with a dialogue
for you to supply the missing information interactively. This is used by xpp
itself to implement the New Editor Session and New Command Session features
and is also useful if you want to set up window manager menu items or desktop
shortcuts to start xpp.

3) When the Command Tool is first popped up, or popped up after being dismissed
with the dismiss button, the keyboard input focus is now directed to the
command line field.

4) When the Search & Replace Tool pops up, the keyboard input focus is now
directed to the last operation button pressed (or the search forwards button
the first time it pops up).

5) If you run xpp as super-user, it now considers that any file that you open
is read-only unless it is owned by super-user and has owner write access.

6) The sash control that used to appear under the replacement text in the
Search & Replace tool was not useful, and had counter-intuitive behaviour
in some cases. It has been removed.

7) A bug with the treatment of "^" in regular expressions has been fixed.

8) The names of the widgets that make up Xpp have been rationalised.
All widget names now conform to the syntax allowed in resource files.
A list of all the widgets (widgets.txt) has been provided for reference.

9) The support for regular expression searching in the GNU and FreeBSD
C libraries has been found to be very slow on long files. A work-around
for this has been implemented.

10) Dialogue boxes such as the Search Tool now conform better to the
Motif style - they are initially positioned more neatly and can be dismissed
using the osfCancel key (typically mapped to the ESCAPE key).

11) If you set the resource Xpp*journal.editable to True, typing in the
journal window automatically pops up the Command Line Tool and your
typing is diverted into that tool.

12) Xpp will now warn you if you the file you are editing has been modified by
some other process since it was last opened or saved by xpp when you ask
to open a new file or to quit. (Previously this condition was only checked
when you asked to save the file).

13) The handling of UN*X signals and X Windows errors has been made more
uniform and more comprehensive.

14) If you insert text into the command line tool containing newlines, e.g.,
by copy-and-paste, the newlines are now converted into spaces.

PPHol:

1) A bug in the Standard ML function oe_enter has been fixed.

2) When compiled with PolyML, the printing order for Standard ML
variables defined in the same binding now defaults to the order
of occurrence. I.e., PolyML.Compiler.printInAlphabeticalOrder
is set false.

PPZed:

1) The treatment of schemas-as-predicates and theta-terms that bind global
variables has been corrected. Such constructs were previously not always
translated correctly (the relevant signature variables became free variables in
some circumstances) and were not pretty-printed as Z.

2) There were two theorems in the theory z_functions that used to
have a free variable. The missing universal quantifiers have been
supplied.

3) The subscript shift character now applies to an immediately
following identifier or decimal number not just the following
character.

PPDaz:

1) PPDaz now has an explicit concrete syntax, "nothing;", for the implicit
null statements that have long been used in its abstract syntax as a
place-holder for a statement that is not present in the actual Ada program
(e.g., in an if statement with no else part).

2) A dollar sign may be used to escape one of the Compliance Notation
reserved words and use it as an Ada identifier.

3) A context clause of a package specification now also applies to the
corresponding package body whether or not the context clause is repeated
for the package body (in accordance with ALRM section 10.1.1). This applies
both to with clauses and use clauses.

4) New functions strings_from_fmt1 and make_output_fun1 are provided in the
structure CNSparkOutput. Together with two new integer controls
cn_left_margin and cn_tab_width, these give extra flexibility to users
programming extensions to the tool which need to map Ada abstract syntax
into concrete syntax. The treatment of the control
cn_automatic_line_splitting has been fixed to match the documentation
(setting it to 0 is now allowed and suppresses line-splitting).

5) The error reports when a specification statement is not type-correct
have been improved. Type-checking now requires the variables in a global
dependency list (Xi-list) in a function specification statement to
be in scope.

6) The parser error reports to do with invalid tags in refinement steps
and replacements have been improved.

================================================================================
2.7.1:

GENERAL:

All packages can now be built and run on Apple PowerPC systems running Mac OS X
as well as on the x86-Linux and Sparc-Solaris platforms.

Thanks to a contribution by John Murdie, the documentation packages for PPXpp,
PPTex, PPHol and PPZed now include manual pages for the UN*X command line
interfaces.

PPDev:

1) The SLRP parser generator is now more powerful and easier to use. It now
implements the LALR(1) algorithm in addition to SLR(1) and so can cope with the
same range of grammars as popular parser generators for C such as bison and
yacc. An API supporting an easy way to evolve from just having a grammar to
having a full parser has been provided and there is a user guide.

PPXpp:

1) Editing text files in MS-DOS and Macintosh format is now supported. A file
type menu is now provided in the options Tool to let you select the format in
which files are saved.

2) Files containing control characters can now be opened by xpp - the
uneditable characters are converted into question marks. This is intended to
help you fix corrupted text files or inspect files containing a mixture of
binary data and text.

3) Case-insensitive and regular expression searching are now supported. These
are selected by toggle-buttons in the Options Tool. An options button has been
added to the Search and Replace Tool to make it convenient to pop-up the
Options Tool to see or change the settings.

4) The Command/Execute Selection menu item no longer requires the selection to
be in the script window.

5) Menu items and buttons that refer to the `selection' can now take the
selection from other X applications that comply with the usual X conventions
for text selections. E.g., other instances of xpp and most standard X
applications that have text fields.

6) Xpp now defends itself against control characters appearing in the output
from the application that is displayed in the journal window.

7) The Command Line Tool now maintains a history of the commands that have been
executed. You can scroll through the history using the Page Up and Page Down
keys.

PPHol:

1) A contribution from Roger Jones which makes GEN_INDUCTION_T and related
tacticals and tactics more general has been incorporated.

2) New theories set_thms and fun_rel_thms have been introduced. These contain
more theorems abouts sets and functional relations, including Zorn's lemma and
the Schroeder-Bernstein theorem.

3) The definition of antisymmetry in the theory orders has been changed so that
it no longer entails irreflexivity. This results in the removal of the theorem
down_sets_dense_thm1 and a change in the statements of the theorems
down_sets_dense_thm and induced_order_antisym_thm. The spelling of the names of
theorems about down-sets has been rationalised. PartialOrder and LinearOrder
have changed their names to StrictPartialOrder and StrictLinearOrder.

4) Some theorems in the theories orders and %bbR% have been changed
to fit in with the policy of not saving theorems with free variables.

PPZed:

1) The symbols for refinement and replacement in the Compliance Notation
(square subset-equals and the three-bar equivalence symbol) are now defined as
valid characters for use in Z specifications.

2) A conversion z_seqd_eq_conv contributed by Phil Clayton to support
reasoning about equations between sequence displays is now provided. It
transforms an equation between two sequence displays into a conjunction of
equations relating the elements of the displays (or into false if the two
sequence displays have different lengths).

================================================================================

2.6.3: [Patch level A: 21/1/2003]

PPTex: None

PPXpp:

1) If the end of the text in the journal window is visible and you resize the
window using the sash button in the separator bar above it, the end of the text
will now remain visible so that resizing in this way does not affect the way
the text is scrolled up when new output arrives from the application being run.

2) There is now a read-only option which is set automatically if you open a
file for which you do not have write access. You can also set this option
yourself if you want to be warned about accidental changes to the file
you are working on.

3) Xpp will now warn you if you try to save a file that has been modified by
some other process since it was last opened or saved by xpp.

4) The Reset button in the Options Tool has been replaced by two buttons
labelled Original and Current. Pressing Original sets the values in the
form to the values in force when the xpp session was started (which is
what the Reset button did in earlier versions). Pressing Current sets
the values to the ones currently in force. The settings in the Options
Tool now only take effect when you press the Apply button (in earlier
versions some of the settings took effect as soon as you changed them).

5) Xpp can now be compiled to support the editres protocol. (Editres is a tool
that lets you examine the widget hierarchy of an X Toolkit application, which
can be useful to help you set X resources). Editres support is not compiled in
by default, since under Linux, a bug in the XFree86 implementation of the Xmu
library needs to be patched for this to be safe. Without the patch, editres
will cause xpp to crash if editres support is compiled in. Editres support is
safe under Solaris.

6) The Status Label in the File Name Bar is now more informative. It now
indicates independently whether the file is new or modified and also indicates
whether the file is read only.

7) The Revert item in the File Menu is now desensitized if the file you
are working on is new (i.e., does not exist in the file system yet).

8) Various optimisations for speed and space have been made. In particular, the
methods used to redraw the journal window visible when it is resized or when
new text arrives have been optimised to reduce unnecessary calculations and
screen refreshes. This greatly improves performance when the application in
the journal window generates a lot of output and avoids screen flicker and
delays under some window manager operations (in particular, when resizing using
KDE or Gnome/Sawfish with the default settings for resize behaviour).

9) The Palette Tool now directs characters to the text window that currently
has the keyboard focus. So, for example, you can use it to enter symbols
into the Command Line Tool.

10) If you use the horizontal layout for an xpp -command session (e.g., by
setting Xpp*mainpanes.orientation to HORIZONTAL in the app-defaults file), you
will find that the panes have been reorganised slightly to give you a few extra
text lines in the journal window.

[Patch level A: a bug in the calculation of the line number displayed in
the file name bar has been fixed. The format of this part of the file name bar
has also been improved.]

PPHol:

1) There is now a facility for checkpointing the state of a theory and its
descendants. This has entailed a few other small modifications, most
notably a small change to the type USER_DATA.

[Patch level A: the checkpointing system no longer imposes the restriction
that all the theories to be checkpointed must be writable.]

PPZed:

PPDaz:

1) The warnings for non-SPARK syntax have been corrected. No warning
is now produced for named number declarations.

2) It is now possible to implement a formal function in a package body when
the corresponding function in the package specification refers to auxiliary
variables.

3) An additional database "xdaz" is available under Poly/ML. This includes
the Compliance Tool together with X/Motif support and the VC browser.
A version of the poly program including X/Motif support is supplied
as an extra on the CD-ROM in the file xpoly.

4) A schema reference in the global dependency list of a function is
now interpreted specially. A schema reference now corresponds to a
single component in the Z function's first argument, given by a
theta-term.

5) A number of features for managing errors have been added or enhanced.
When a Compliance Notation clause is processed, a checkpoint is taken
of the theory "cn" and its descendants, and if an error occurs, the state
of the theory hierarchy under "cn" is restored. This means that it is now
always possible to correct and re-enter a clause after a previous
failed attempt. A flag cn_stop_on_exceptions can be used to enable
a simple error recovery scheme so that all the declarations and
statements in a clause can be checked even if earlier declarations or
statements contained errors. A log of errors is now maintained for
each script and functions are provided to inspect and manage these logs.


================================================================================

2.6.2:

PPTex: None

PPXpp:

A problem with the undo/redo feature which was causing unpredictable
behaviour has been fixed.

A bug which caused xpp to go into a loop printing an Xt warning message
under some circumstances has been fixed.

The Palette Tool now throws the keyboard focus back to the script window
after you click on a symbol button. This means that you can interleave
typing and selecting symbols from the palette without needing to
reselect the insertion position in the script window.

PPHol: None

PPZed: None

PPDaz:

A new function delete_script allows you to remove a script from
a compliance argument, e.g., to modify and reload it, without having
to reload scripts that are not dependent on it.

A new flag cn_spark_syntax_warnings is provided which you can
use to enable a check on whether your Ada code conforms to
the context-free grammar given in "High Integrity Ada: the SPARK
Approach".

You can now use block statements freely in code that is not
being processed formally. The rule that a block statement
must appear on its own on the right-hand side of a refinement
or replacement step still applies if you want the block
statement or the declarations in it to be processed formally.

A bug in the handling of subtypes of record types with
discriminant constraints has been fixed.

================================================================================

2.6.1:

This is the first open source release. There are cosmetic changes
to the source of all the packages. A number of bugs and infelicities
in PPXpp have been fixed. The other packages have no functional changes.

================================================================================
2.5.11:

PPTex: None

PPXpp:

1) Xpp now includes the name of the file you are working on in in the window
title bar as well as in the icon title. This is intended to be nicer with twm,
fvwm, KDE, and many other window managers which use the title bar title rather
than the icon title to identify an application.

2) If the application in the xpp journal window dies, the last bit of output
from the application used to get discarded. This omission has been fixed.

3) There is now no limit other than operating system memory limits
on the amount of text that can be executed by the Command/Execute
Selection (Ctrl-X) menu option. (In earlier versions there was a fixed
limit of 40,000 characters).

4) The current line number is displayed in the file name bar next to
the ProofPower logo. This feature may degrade response times when working
with very large files or on slow processors with limited physical
memory. The degradation is imperceptible on, say, files up to 10Mb
on a 450MHz processor with 256Mb of RAM. If you do experience problems,
you can turn off line number tracking by right-clicking on the line
number label.

PPHol:

1) new_flag, new_int_control and new_string_control now gives a warning rather
than a failure in the case where the flag or control already exists. If the
flag ignore_warnings is true, or if you answer `y' interactively when asked
whether to continue, the old flag or control is renamed (by decorating the old
name with 1 or more prime characters) and the new flag or control is added with
the specified name.

PPZed: As for PPHol

PPDaz: As for PPZed plus:

1) Default parameters to functions and procedures are now supported
provided the default expression contains no program variables.

2) Block statements are now supported. Block statements must
occur on their own on the right-hand side of a refinement or
replacement step.

3) The frames of logical constant statements were not being
checked in some circumstances. This bug has been fixed.

4) Record aggregates in qualified expression where the qualifying
type mark is a simple name introduced by a use clause were
not being handled properly (usually resulting in Z type-checking
errors). This bug has been fixed.

5) Incorrect VCs were being generated in some circumstances
where a procedure call was proceeded by other code. This bug
has been fixed.

6) Assertions are supported. An assertion is a kind of specification
statement with no post-condition and no frame introduced by
a capital gamma rather than a capital delta. An assertion is
allowed wherever a statement is allowed.

7) The Poly/ML binaries have been compiled under Poly/ML version
4.3. The new Poly/ML flag PolyML.Compiler.printTypesWithStructureName
is set false by default in the ProofPower ML databases.

8) Renaming of operator symbols where the original name has
no package name prefix is now supported.

================================================================================

2.5.10:

PPTex: None

PPXpp: None

PPHol: None

PPZed:

1) Several new theorems and a new induction tactic have been added
relating to Z sequences (in the theory z_sequences1).

PPDaz:

1) Ada constant declarations are now translated into Z axiomatic
descriptions rather than abbreviation definitions. This makes
the Ada type information in a constant declaration available
for reasoning about the constant.

2) In some circumstances, the checks on accesses to global variables
from procedures in package bodies were previously being circumvented.
This bug has been fixed.

3) Several deficiencies in the treatment of renaming declarations have
been fixed.

4) The treatment of use clauses has been changed to give more generality and a
better fit to the Ada scoping rules. Use clauses no longer give rise to Z
abbreviation definitions.

================================================================================

2.5.9:

PPTex: None

PPXpp: None

PPHol:

1) The efficient dictionary data type (E_DICT) now supports access
functions e_key_lookup, e_key_extend etc. that are more efficient
if the same string is to be used as an index into several dictionaries.

2) A new type of order-preserving dictionaries (OE_DICT) has been
provided. This combines the functionality of the E_DICT and
S_DICT data types.

3) The ML representation of theories has been enhanced
to make a number of operations more efficient. Associated with
this change are three new theory access functions get_defn_dict,
get_thm_dict and get_axiom_dict.

4) A "stopwatch" timer facility has been implemented to make it easier
to time sequences of ML commands that are not packaged up as a function
(see read_stopwatch in the Reference Manual).

5) The sort function (Sort.sort) and the string ordering function
(Sort.string_order) now use more efficient algorithms.

PPZed:

1) There have been code changes to allow for the changed representation
of theories but no functional changes.

PPDaz:

1) A bug has been fixed in the checks on certain constructs that must appear
first in their sequence of statements (see USR504, Compliance Tool Language
Description, section 3.3).

2) The treatment of use clauses has been liberalised.

3) Several bugs in the treatment of renaming clauses have been fixed.

================================================================================

2.5.8:

PPTex: None

PPXpp:

1) It is now possible to undo and redo multiple changes to the file being
edited.

2) An error in the font `holsans10' has been corrected (the Z injection arrow
had the wrong shape) and the appearance of some of the characters has been
improved.

PPHol, PPZed:

1) The Reader/Writer (the preprocessor that converts ProofPower-ML into
Standard ML) has been changed to avoid passing long string literals to the
Standard ML compiler. This results in a significant improvement in performance
when processing very long object language quotations.

PPDaz:

1) The performance of the lexical analyser has been improved. In conjunction
with the PPHol and PPZed performance improvements this means that it is now
feasible to input large fragments of Ada code without breaking them up into a
large number of separate web clauses.

2) The syntax-check-only mode has been extended to support storage and output
of the Ada program and to support all the Compliance Notation features for
literate programming. Pre- and post-conditions and other fragments of Z in a
script are parsed in this mode but not type-checked.

3) The restriction that aggregates must be given as qualified expressions no
longer applies to aggregates used as the initial values of variables and
constants.

================================================================================

2.5.7:

PPTex: None

PPXpp:

1) The yes/no/cancel dialogue that is popped up when a selection to be executed
does not end in a new-line now works properly.

2) A new font `holsans10' is available. This is a 10-pt sans-serif font that is
suitable for medium resolution screens (e.g., 1024x768 pixels on a 14' or 15'
laptop screen).

PPHol:

1) A bug in the printing of `Q's in file names has been fixed.

PPZed:

None.

PPDaz:

1) Use package clauses and all the forms of renaming declarations other than
exceptions are now supported formally provided they do not introduce duplicate
names into the name space.

2) Ada '95 use type clauses are now supported.

3) Discriminant parts and discriminant constraints are now supported formally.

4) The full Ada syntax for exit, exit-when and return statements is now
supported formally, including return statements in procedures. The
restrictions that required return statements in particular places in functions
have been dropped.

5) A subprogram declaration for a subprogram whose body will be provided later
in the same declarative part is now supported formally. This includes
full formal support for recursive and mutually recursive procedures and
functions.

6) A package name may now appear more than once in the with clauses at the head
of a compilation unit.

================================================================================

2.5.6:

PPTex: None

PPXpp: None

PPHol:

1) pp_make_database now accepts the parent database name with or
without the compiler/architecture-dependent suffix.

PPZed: None

PPDaz:

1) Capital `Q's are now pretty-printed properly by the Ada output
functions.

2) Capital `Q's in Ada strings are now translated properly.

================================================================================

2.5.5:

PPTex: None

PPXpp:

1) When started with the name of a non-existent file, xpp now gives you an
option to start editing an empty buffer with the file name set to the name of
the non-existent file.

2) A bug in the command-line processing has been fixed: you may now omit the
-file and -command option keywords. "xpp <file> <cmd> <args>" is equivalent to
"xpp -file <file> -comand <cmd> <args>".

3) xpp now sets the environment variable PPLINELENGTH to the width of the
journal window when the command is started or restarted. This effect can be
overridden by setting the environment variable explicitly before invoking xpp.

PPHol:

1) The function ExtendedIO.execute has been withdrawn and replaced by
ExtendedIO.system. The interface offered by ExtendedIO.execute did not allow
the spawned process to be reaped properly on termination. Equivalent
functionality to ExtendedIO.execute is available in the Standard ML Basis
library, if required.

2) The initial value of the line_length integer control is taken from the
environment variable PPLINELENGTH if that is set and contains a decimal integer
greater than 19. This control determines the length of lines produced by
various listing facilities such as print_theory.

3) A number of bugs have been fixed relating to ProofPower-HOL aliases.
undeclare_alias may now be used effectively to hide a constant name.

4) The scripts pp and pp_make_database have had a number of bug fixes and
enhancements. Thanks to Phil Clayton of QinetiQ for many of these. See the
reference manual pages for these scripts for more details.

5) A number of bugs in the system initialisation functions have been fixed. In
particular, the state of the system controls module (which manages flags,
integer controls and string controls) is properly preserved now.

6) The obsolete script pp_read has been withdrawn and is no longer supplied.

PPZed:

1) The implementation of the Z library no longer undeclares the aliases for the
HOL integer arithmetic operations.

2) Consecutive underscores are now allowed inside Z identifiers.

PPDaz:

1) The symbol for expansion of a statement label (i.e., for an informal
refinement step) has been changed to a refinement sign preceded by an
exclamation mark. This prevents the conceptual overloading of the symbol used
for expanding declaration k-slots, and means that all informal development
steps contain an exclamation mark.

2) SPARK program output function bug fixes: if a formal parameter mode is
omitted in the original Ada code, then it is now printed without an explicit
mode when the program is printed. All forms of loop statement are now pretty
printed correctly as are percent signs in string literals.

3) VC generator fixes: type conversions using the pre-defined real types are
now translated into Z correctly. A bug which prevented the same name being used
for formal parameters of different types in different subprograms under some
circumstances has been fixed.

4) A number of bugs which caused problems to do with the database hierarchy
under Poly/ML have been fixed.

5) A package name may now be given several times in a context clause.

6) The global variable INFORMAL_FUNCTION in the theory cn has been renamed to
Informal_Function to avoid the possibility of a clash with an Ada name.

7) The soundness checks made when the program is printed now allow a function
to end in a case statement without an others part. When the checks fail, the
program is now printed (or output) in its entirety.

8) The array sliding conversion introduced in version 2.5.4 is now also
being applied when array and record aggregates are used to construct
arrays of arrays.

================================================================================