Derrick, John
Unknown Affiliation

Published : 1 Documents Claim Missing Document
Claim Missing Document
Check
Articles

Found 1 Documents
Search

Translations of Embedded Theorems in Z Specifications Siregar, Maria Ulfah; Derrick, John; Yazid, Ahmad Subkhan
IJID (International Journal on Informatics for Development) Vol. 5 No. 2 (2016): IJID December
Publisher : Universitas Islam Negeri (UIN) Sunan Kalijaga Yogyakarta

Show Abstract | Download Original | Original Source | Check in Google Scholar | Full PDF (240.873 KB) | DOI: 10.14421/ijid.2016.05205

Abstract

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.