Extending Operation Semantics to Enhance the Applicability of Formal Refinement
This paper proposes an extension of operation semantics and discusses its benefits in enhancing the applicability of Morgan’s formal refinement calculus in practical software development.
- PDF / 141,131 Bytes
- 7 Pages / 439.363 x 666.131 pts Page_size
- 7 Downloads / 234 Views
Abstract. This paper proposes an extension of operation semantics and discusses its benefits in enhancing the applicability of Morgan’s formal refinement calculus in practical software development.
1
Introduction
Morgan established the refinement rule for developing sequential programs in [1]. Let A : s [Apre , Apost ] be an operation that changes the the initial state s (a set of variables subject to change) to a final state s satisfying the postcondition Apost , provided that the precondition Apre is true before the operation. If operation B : s [Bpre , Bpost ] refines operation A, denoted by A B, then the refinement rule containing the following two conditions must be satisfied by A and B: (1) Apre ⇒ Bpre (2) Apre ∧ Bpost ⇒ Apost The rule states that operation B weakens the precondition and strengthens the postcondition of A. The rational behind the rule has been well described by Morgan in [1] and the rule has been widely accepted by the formal methods community [2,3,4,5]. While the application of the rule disallows an operation to be refined into an incorrect executable program, it allows a feasible (or satisfiable) operation to be refined into an infeasible operation in the process of a successive refinements leading to code. By infeasible operation we mean that the operation is impossible to be satisfied by any normally executable program (i.e., a program defining a function). Such a refinement may have a negative impact on software development in practice. For example, consider the operation F : {x}[x = 0, x > 0 ∧ x = x + 1 ∨ x < 0 ∧ x = x + 2] where x is an integer. F can be refined into the operation H : {x}[true, x > 0 ∧ x = x + 1] because both operations F and H satisfy the refinement rule, that is, Fpre ⇒ Hpre Fpre ∧ Hpost ⇒ Fpost
This work is supported in part by the SCAT research foundation and Hosei University.
S. Iida, J. Meseguer, and K. Ogata (Eds.): Futatsugi Festschrift, LNCS 8373, pp. 434–440, 2014. c Springer-Verlag Berlin Heidelberg 2014
Extending Operation Semantics to Enhance the Applicability
435
However, there are two problems with operation H. Firstly, it is not desired with respect to operation F because it does not do exactly what F requires (e.g., when x < 0, F requires that the state variable x be increased by 2, that is x = x + 2, but operation H offers no definition). Secondly, H is infeasible, that is, it is impossible to refine H into a normally executable program (An extreme example is to refine operation H into a “miracle” : H m : {x}[true, f alse]). This situation has the following three implications for real software development: – The refinement rule does not guarantee that an operation will be refined into a correct program (i.e., a program that is both normally executable and satisfying its operation specification), although it guarantees that the operation will not be refined into an incorrect program (i.e., a program that is either not normally executable or not satisfying its operation specification). For this reason, the refinement rule must be used with caution; otherwi
Data Loading...
