Constructive Z
S-H Mirian-Hosseinabadi · Journal of Logic and Computation · 1998
An approach to Z-style program specification is developed based upon a constructive version of Zermelo-Fraenkel set theory without replacement. The idea of obligation schema, an extension of Z-schema, is introduced, and an implementation of this notion presented which facilitates the abstraction of programs.