Inductive definitions in COLD-K

Abstract

This paper reports on the form and the logical semantics of inductive definitions in the wide-spectrum design language COLD-K. It is shown how and when predicate definitions of the form the smallest P satisfying property A(P) can be transformed into monotonic predicate functions with P as their least fixpoint.