Translations of Embedded Theorems in Z Specifications | Zendy

Maria Ulfah Siregar | Zendy; John Derrick | Zendy; Ahmad Subkhan Yazid | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Translations of Embedded Theorems in Z Specifications

Author(s) -

Maria Ulfah Siregar,

John Derrick,

Ahmad Subkhan Yazid

Publication year - 2016

Publication title -

ijid (international journal on informatics for development)

Language(s) - English

Resource type - Journals

eISSN - 2549-7448

pISSN - 2252-7834

DOI - 10.14421/ijid.2016.05205

Subject(s) - programming language , equivalence (formal languages) , computer science , algebra over a field , discrete mathematics , calculus (dental) , mathematics , pure mathematics , medicine , dentistry

This paper discusses our proposal on how to embed theorems in Z specifications. One reason behind this proposal is to ease Z users in writing theorems directly in their Z specifications. Another reason is not to overwhelm Z users in learning other language, which in this case is SAL language. In doing so, we need to inform Z2SAL programmers how to translate these embedded theorems into equivalence theorems in SAL specifications. Based on our experiments, Z2SAL is able to translate these kind of theorems and SAL model checker is also able to model check SAL specifications with theorems that are written directly in the Z specifications.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research