Generating Python Code From Object-Z Specifications

TL;DR

This paper proposes a method to translate Object-Z specifications into Python code, enabling validation of system properties like preconditions, post-conditions, and invariants using Python's features.

Contribution

It introduces a novel mapping from Object-Z to Python that supports key constructs and formal validation, leveraging Python's functional programming capabilities.

Findings

Python effectively supports Object-Z specification mapping.

The approach enables validation of invariants and conditions in Python.

Python libraries can be developed for Object-Z to Python translation.

Abstract

Object-Z is an object-oriented specification language which extends the Z language with classes, objects, inheritance and polymorphism that can be used to represent the specification of a complex system as collections of objects. There are a number of existing works that mapped Object-Z to C++ and Java programming languages. Since Python and Object-Z share many similarities, both are object-oriented paradigm, support set theory and predicate calculus moreover, Python is a functional programming language which is naturally closer to formal specifications, we propose a mapping from Object-Z specifications to Python code that covers some Object-Z constructs and express its specifications in Python to validate these specifications. The validations are used in the mapping covered preconditions, post-conditions, and invariants that are built using lambda function and Python's decorator. This work has found Python is an excellent language for developing libraries to map Object-Z specifications to Python.