Known Bugs
The following is a list of known bugs and other
issues, which
are being dealt with as time allows.
User Interface Issues
Here we will list any requests to modify the user interface of
the tool.
Input Parsing Issues
Here we will list examples of inputs that we should parse, but
currently cannot.
- The public beta-version of the tool does not yet translate Z
sequences (because we haven't yet tested all the sequence operations).
However, in the alpha-version of the tool, we have successfully
translated sequence operations. Users may submit a Z2SAL translation request if they wish to see what an
example with sequences looks like.
Output Generation Issues
Here we will list examples of incorrectly-generated SAL output,
which may cause the SAL tools to object.
The following are points of style, or a wish-list of things to do,
rather than semantic errors:
- In the regular "Translate Z into SAL" for model-checking purposes, it
is redundant to specify, in the
ELSE clause, that certain
posterior primed variables retain their unprimed values. If we don't
mention any primed variables after the --> arrow, then the
tools ensure that they keep the same values as before, anyway.
- When translating the Kurbel and Marlowe refinement, the generated
SAL context
tickets_app_and_corr.sal contains a stylistic
quirk, which is not an error. The free type MTicket has
a different automatic label,
label__1, from the label__0 that was
generated in the other context tickets_init.sal.
As it happens, references to the label throughout each context are
consistent, but it is just odd that the free type is defined
slightly differently in each of the two contexts.
- In the refinement checking
XXX_init.sal examples, it
would be nice in future if the retrieve relation could be generated as
a DEFINITION, in a similar way to the
XXX_app_corr.sal examples. This would make it much easier
and formulaic to write the initialisation theorem, which could also
be generated automatically.
Library Encoding Issues
Here we will list any known issues with the SAL encoding of the Z
mathematical toolkit.
| 
