[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

problem of pvs to z specification



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