TY - GEN
T1 - A logical framework for evolution of specifications
AU - Li, Wei
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.
PY - 1994
Y1 - 1994
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84998637038
U2 - 10.1007/3-540-57880-3_26
DO - 10.1007/3-540-57880-3_26
M3 - 会议稿件
AN - SCOPUS:84998637038
SN - 9783540578802
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 394
EP - 408
BT - Programming Languages and Systems - ESOP '94 - 5th European Symposium on Programming, Proceedings
A2 - Sannella, Donald
PB - Springer Verlag
T2 - 5th European Symposium on Programming, ESOP 1994
Y2 - 11 April 1994 through 13 April 1994
ER -