Proving correctness of constructor implementations

Jordi Farres-Casals

Abstract: In [ST 86] the notion of constructor implementation was introduced generalizing previous well-known implementation definitions such as in [EKMP 82]. In this paper we explore a proof strategy for this kind of implementation in a specification language close to ASL. The results show that these proofs are feasible in some cases, but since a general result is not attainable we are satisfied by coping with the most common cases.


Previous | Index | Next