Premium
An exercise in program design using SIMULA class invariants
Author(s) -
Cunningham B. J.,
Kramer T.
Publication year - 1978
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.4380080311
Subject(s) - simula , assertion , correctness , computer science , representation (politics) , invariant (physics) , scheduling (production processes) , bounded function , programming language , theoretical computer science , mathematical optimization , mathematics , political science , law , mathematical physics , mathematical analysis , politics
The concept of an invariant assertion has been shown by Hoare to be central to the problem of proving correctness of data representation in a program. A consequent approach for program design is to establish the parts of an overall invariant which characterize the components of the design. In this way it is feasible to synthesize a verified program. There is a gulf between verification theory and practical reality in this area, but the SIMULA class concept is close to the data representation technique required for such an approach. Some of the benefits and problems of this approach to design have been explored by the development of a SIMULA program to simulate a bounded delay resource allocation strategy in a job scheduling environment.