Abstract
A logical framework of software evolution is built. The concepts of sequence of specifications and the limit of a sequence are established. Some concepts used in the development of specifications, such as new laws, user's rejections, and reconstructions of a specification are defined; the related theorems are proved. A procedure is given using transition systems. It generates sequences of specifications from a given user's model and an initial specification. It is proved that all sequences produced by the procedure are convergent, and their limit is the truth of the model. Some computational aspects of reconstructions are studied; an R-calculus is given to deduce a reconstruction when a specification meets a rejection. An editor called Specreviser is introduced. It is used to develop specifications. The main functions of the editor are given; some techniques used in its implementation are also discussed. Finally, the theory is compared with AGM's theory of belief revision.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alchourrón, C.E., Gärdenfors, R. and Makinson, D., On the logic of theory change: partial meet contraction and revision functions, The Journal of Symbolic Logic, Vol.50, No.2, June, 1985.
Eiter, T. and Gottlob, G., On the complexity of prepositional knowledge base revision, Artificial Intelligence, Vol. 57, October, 1992.
Gallier, J.H., Logic for Computer Science, foundations of automatic theorem proving. John Wiley & Sons, 1987, 147–158, 162–163, 197–217.
Garey, M.R. and Johnson, D.S., Computers and Intractability, Freeman and Company, 1979.
Li, W., An Open Logic System, Scientia Sinica, Series A, Oct, 1992 in Chinese, March, 1993 in English.
Li W., A Theory of Requirement Capture and its Applications, TAP-SOFT'93, LNCS 668, 1993, Springer-Verlag.
Paulson, L., Logic and Computations, Cambridge University Press, 1987, 38–50.
Plotkin, G., An structural approach to operational semantics, Lecture notes, Arhus University, Denmark, 1982.
Shoenfield, J.R., Mathematical Logic, Addison-Wesley, Reading, Mass, 1967, 74–75.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, W. (1994). A logical framework for evolution of specifications. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_26
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive