1

I have seen some papers that describe how to use the Z notation with Isabelle/HOL using the tools HOL-Z and ZETA. I was not able to find these tools, have they ever been published? Are there other ways to use Isabelle with the Z notation?

dordow
  • 115
  • 6
  • Never heard of those. Can you provide a link to a paper? Maybe contact the authors of the papers directly? – Mathias Fleury Nov 02 '21 at 07:46
  • 1
    Here is one: [HOL-Z 2.0: A Proof Environment for Z-Specifications](http://www.jucs.org/doi?doi=10.3217/jucs-009-02-0152) – dordow Nov 02 '21 at 19:22

1 Answers1

0

If you are prepared to substitute Isabelle/HOL for one of the HOL theorem provers (which also adopt the LCF approach to soundness) then you should consider ProofPower, which also embeds the Z notation in HOL. ProofPower-Z has been used on large industrial examples for many years, in particular to discharge verification conditions to show the correctness of Ada source code.

Phil Clayton
  • 1
  • I have heard of ProofPower and had a look into it. It uses a markup language with special characters but I would prefer a pure ASCII markup, ideally solely based on LaTeX. – dordow Nov 14 '21 at 17:24
  • Whether you tell ProofPower to work with UTF-8 or its own bespoke character encoding, you can always write ASCII mark up with %...% sequences. These have some similarity to the LaTeX sequences - the mapping can be found in the file /etc/sievekeyword. Note that these escapes can be used in ML names too, which makes PPML different from SML. Personally, I find the Unicode characters much more readable. Consider ⓩ∀ x : ℤ ⦁ 0 ≤ x⌝ vs. %SZT%%forall% x : %bbZ% %spot% 0 %leq% x%>%. – Phil Clayton Nov 15 '21 at 20:42
  • Well thank you for the hint. I am used to something like \begin{szt}\forall x : \num @ 0 \leq x \end{szt}. Maybe I could define some macros and preprocess before calling the ProofPower tools. – dordow Nov 17 '21 at 22:03