problem of pvs to z specification

[Bing Wu <B.Wu@scm.brad.ac.uk>]

Hi, I am PhD student of University of Bradford. I am studying Formal
Methods. And I am trying to use PVS to process my Z specification. But I
meet some problem in converting Z specification to PVS specification.
Could you please help me with this:

\begin{schema}{NewAccount}
  \Delta Bank \\
  users? : \powerone Client \\
  id! : ID
\where
  id! \notin accounts
\also
  \exists Account' \mid OpenAccount
 @ account' = account \oplus \{ id! \mapsto \theta Account' \}
\end{schema}

Thank you very much!

Bing Wu
 Bsc Msc Phd
 School of Computing and Mathematics
 University of Bradford
 Bradford, West Yorkshire, BD7 1DP, UK
 Telephone: 01274-233934
 Email: b.wu@scm.brad.ac.uk

---

• Prev by Date: Re: Bogus << TCC
• Next by Date: Q: list
• Prev by thread: Q: list
• Next by thread: Re: problem of pvs to z specification
• Index(es):
  • Date
  • Thread