BEYOND STRUCTURED PROGRAMMING
Contents
1. 3 3 1 Basic Normalization Conditions for Loops The general requirements are designed to ensure that the context defined by the precondition P and the guard G really warrants the use of a loop that has the potential to execute more than once and to terminate The precondition P here is not the loop invariant but rather a condition established by the loop initialization which will always strictly imply the strongest loop invariant for the loop LBN 1 gt 3G LBN 2 LBN 3 sp P do G S od P a G OE AG este IAG S gt G LBN 1 The first normalization condition LBN 1 requires that the loop is reachable for all possible initial states under which it must execute That is there must be no initial state defined by a non grounded precondition P for which the loop guard is false LBN 2 The condition LBN 2 deals with the efficiency of a loop It is different to LBN 1 in that the loop may execute a number of times however it demands that the loop establishes more than simply the negation of the loop guard without changing the precondition P For example the loop P do i N i i 1 od should be avoided because it produces only the condition i N even though it may execute a number of times LBN 3 Any loop to be deserving of that status should have the potential to execute more than once for a given non grounded precondition P and guard G This requires not only that the loop is reachable but also tha2. of tree structures with cycle nodes then for a simple cycle that contains no subcycle a local variable is needed to decompose this cycle into a tree However a more complex process 13 is needed to handle a complex cycle that contains nested subcycles oll c The three implementations below illustrate the impact of applying variable normalization The normalized implementation RaGCD uses six rather than the seven or eight assignments used in the other two implementations In Ra6CD each variable is used only for a single purpose Example Two implementations ExGCD1 and ExGCD2 of the extended Euclid s GCD algorithm have been presented by Jensen amp Wirth 6 and Horowitz amp Sahni 7 respectively ExGCD1 ExGCD2 c M d N x 0 y 1 c M d N x 0 y 1 do dz0 gt do 1 gt q c d r cmodd q c d r cmodd y y q x c d d r X X y y T od retum y x y y w od w x q y c d d r if y lt 0 gt y y p fi return y RaGCD c M d N x 0 y 1 do 0 gt prex x prec c x y c d x y prex c d d precmodd od retumn y After applying equivalence transformations we get q r c d x y c d x d cmodd y c d x x from the loop body of ExGCD1 After removal of local variables q and r we obtain the underlying logical intent of the body that is c d x y 275 d cmodd y c d x x Its VDDG and normalized result RaGCD are as follows f2 f2 a e d
3. to its precondition This constitutes a normalization condition for assignments If an assignment does not satisfy this requirement it is redundant and may be removed from the computation without consequence We may express this normalization condition formally using strongest postconditions We define sp P S to represent the strongest postcondition 2 13 established by the statement S when it executes in the context of the precondition P For an assignment S executing in the context of the precondition P we require NAS 1 sp P S P to be satisfied for the assignment to be normalized Otherwise such an assignment S must be a self assignment e g x x or establish an already established condition It is straightforward to do a strongest postcondition calculation to determine whether an assignment is normalized 3 2 If Statements It is important to apply semantic normalization techniques to branch statements to avoid all the potential insecurities and correctness problems with such statements To ensure that a branch structure is normalized three types of condition must be considered the precondition P the set of branch guards C1 C2 CN and the set of conditions D1 D9 DN that apply after each branch has executed Here we consider branch statements of the form 4 P if Ci gt S81 D1 O C2 gt S2 D2 D O CN gt SN Dn fi For such a statement to be normalized we suggest that the follo
4. to set another variable y that can be used in another branch test in the statements that follow However we may use x 0 and x 0 to replace this additional test This is possible because in one sense this branch statement establishes another flag y from the original flag x When the disjunctive postcondition D v D9 can be simplified into an equivalent conjunctive form D there are two cases that apply One is that the weakest branch postcondition Dj is equivalent to D and another D implies D as Dy vD2 Dv Dj D where je 1 2 Another case is that both of the branch postconditions Dy and D imply D and each of them has an extra part R i e Dj D A Rj for ie 1 2 which satisfies Ry v R true We suggest that the normalized branch statement should be classified according to the first case rather than the second case Because from a theoretical viewpoint these R do not appear in the postcondition they may be used only for branching purposes otherwise they are redundant From a technical view point if these Rj are needed for the branch statement as branch conditions the branch conditions or their modifications of the original branch statement that produces these Rj may replace them For example if x 0 x 1 flag true x40 gt x x 1 flag false fi is not a normalized branch statement under any precondition P x because sp P x if x 0 x 1 flag true x 0 x x 1 flag false fi P x 1 a x 1 flag
5. we can build a Variable Dependency Directed Graph VDDG The formal definition is Given any multiple assignment x f its VDDG is a directed graph containing a node set x and an edge set lt x y gt x f e x f ye V f x i e variable x connects to all its dependent variables except itself where V f is the variable set of f This graph cannot contain any self cycles The problem of determining the maximum number of local variables may be translated to determining the number of local variables that convert a multi assignment into an implementable assignment sequence in an imperative program Two cases apply for the VDDG They are the VDDG is a tree or a number of trees without any cycles the VDDG is a tree structure or a number of tree structures with cycle nodes When a given VDDG is a tree or a number of trees no local variable is needed because we can use an extended Pre Order traversal of the tree to decompose the corresponding multi assignment into a normal assignment sequence This order also defines the principle for decomposing any directed graph with cycle nodes The following diagrams illustrate these ideas ee multi assignment a b c d e Pc e f ar de s t v d d a p c e f z yea decompose P c r d e Pal f feee c we P a p c e f f d b q f d e f c r d e P b a0 deco Saat c r de a d s f e t d f f v f When a VDDG is a tree structure or a number
6. BEYOND STRUCTURED PROGRAMMING S Pan R G Dromey Software Quality Institute Griffith University Nathan Qld AUSTRALIA 4111 Abstract Structured programming principles are not strong enough to control complexity and guarantee high reliability of software at the module level Stronger organizing principles and stronger properties of components are needed to make significant gains in the quality of software Practical proposals based on the definition of normal forms which have a mathematicalllogical foundation are suggested as a vehicle for constructing software that is both simpler and of higher quality with regard to clearly defined and justifiable criteria 1 Introduction Stronger principles of programming at the module level are needed if we are to make significant gains in controlling the complexity of software improving its reliability and its overall quality Structured programming 3 modularization techniques and information hiding 15 and abstract data types 9 have all made important contributions to this end However when we ask things like What belongs and what does not belong in a loop body Is there an implementation for this algorithm that has a smaller McCabe Number What is the ideal structure for a sequence of statements How many local variables are needed to implement this algorithm or Is a given module cohesive or should it be split into two or more smaller modules we find
7. Base Systems Computer Science Press 1988 277
8. anguages and compilers References 1 10 11 12 13 14 15 16 Birkhoff G MacLane S Algebra MacMillan N Y 1967 Dijkstra E W Scholten C S Predicate Calculus and Program Semantics Springer Verlag 1989 Dahl O J Dijkstra E W and Hoare C A R Structured Programming Academic Press N Y 1972 Dromey R G Program Derivation Addison Wesley Press 1989 Dromey R G Cornering the Chimera IEEE Software Jan 1996 Horowitz E Sahni S Fundamentals of Computer Algorithms Computer Science Press Inc 1978 Jensen K Wirth N PASCAL User Manual and Report 2nd ed Spring Verlag 1974 Kleene S C Mathematical Logic Wiley N Y 1967 Liskov B H Zilles S N Programming with Abstract Data Types SIGPLAN Notices 9 4 50 59 Apr 1974 Manna Z Properties of Programs and the First Order Predicate Calculation JACM 16 2 1969 McDermid J A Software Engineer s Reference Book Butterworth Heinemann 1991 Myers G Software Reliability Principles and Practices Wiley NY 1976 Pan S Software Quality Improvement Specification Derivation and Measurement Using Formal Methods PhD Thesis Griffith Uni Australia 1995 Pan S Dromey R G Re engineering Loops Computer Journal accepted for pub Parnas D L On the Criteria to be Used in Decomposing Systems into Modules Comm ACM 5 12 1053 1058 Dec 1972 Ullman J D Principles of Database and Knowledge
9. er the precondition p y Ax f a A p a yields ap y Ax f a a a p a A p f a for skip and p y ax aa p a ap f a for the execution of the loop do p x x f x od because after the first iteration the loop guard p x fails Therefore sp p y ax f a a p a if p x gt x a do ap x x f x od fi ap y ax f a ap a a p f a v Gp y ax an p a ap f a aply ax f a ap a sp p y ax f a a p a According to the condition NMB 6 the branch statement can be replaced by the empty statement More generally a normalized branch statement should satisfy the requirement that there exists no simpler statement S than the branch statement such that sp PAC 1 S1 v sp PAC S2 v v sp PACN Sy sp P S NMB 7 The normalization conditions NMB1 6 define a number of requirements for a normalized branch statement The normalization condition NMB 7 differs from these requirements in that it requires that a branch statement should have a unified functionality This condition may be expressed by requiring that the postcondition should be equivalent to a conjunctive condition if the precondition is conjunctive To understand this consider a two branch statement a x Ab z if x 0 y M x40 gt y M 1 fi as an example Obviously the postcondition a x Ab z x OAy M v x 0ay M 1 cannot be simplified to a conjunctive form without any disjunctive term Often programmers use this sort of device
10. esent work could be interpreted as suggestions for normal forms It is however possible to extend these proposals by taking a more rigorous look at module cohesion and the use of variables within modules The application of normal forms corresponds to the imposition of more stringent logical and structural constraints on software components In one sense we are suggesting that more order should be imposed on program structures Our intent here is to rigorously define a set of normal forms for program structures Before presenting our suggestions let us first look at the most well known form associated with program structure the proposals for structured programming which constitute a normal form They require that every type of executable statement has a single point of entry and exit Imposition of this constraint has made an important contribution to simplifying the structure of imperative programs Languages like Modula 2 have chosen to use a language architecture that directly implements and enforces structured programming An obvious question to ask is is structured programming the only normal form relevant and applicable to program structure We contend that this is not the case That in fact there are a number of compatible normal forms relevant to program structure which can be superimposed to yield further important refinements for improving the structural quality of programs The suggestions we will make are intended to simpli
11. ess first we transform the branched statement simple or compound to its base form and then we perform a semantic analysis to determine whether the structure is already normalized 269 3 Normal Forms for Statements It is possible to define normal forms for each type of statement both simple and compound that we encounter in conventional imperative programming These normal forms express an ideal for representing the given statement with respect to well defined and testable criteria They are designed to achieve four outcomes ensure the inherent consistency and problem independent correctness of the statement is preserved minimize its complexity maximize its efficiency and maximize analyzability An additional requirement is that it should be possible to automate the process of transforming a statement into its normal form We will now examine the normal forms for several key program components to illustrate the method 3 1 Assignments Assignments are the simplest building blocks of imperative programs An obvious syntactic requirement for an assignment is that all variables used in its expression should be initialized and there should be no side effects in the expression Apart from these requirements there is only one semantic obligation on an assignment It is that assignments should always advance a computation By this we require that the postcondition established by an assignment should not be equivalent
12. f the sequence The rest of the sequence contains only assignments and write statements that form a lt Omos gt sequence This leads to a new optimized sequence that satisfies the following definition 273 NNIS 2 Bounded Minimum Optimization Structure lt Opmos This is a redundancy free sequence which starts with a number of one or more read statements followed by a sequence in lt Omog gt where each variable is assigned once either by a read statement or an assignment In EBNF we have lt Opmos gt read x lt Omog gt read x lt Opmos gt We may extend any non iterative statement sequence consisting of assignments I O statements to include if statements When all branch guards of an if statement depend on at least one read variable these branch guards are not pre determined for arbitrary input Several transformations 13 exist which enable us to locate such an if statement in front of all statements that follow the read statements which initialize at least one read variable that appears in the branch guards The encapsulating structure starts with a number of one or more read statements followed by an if structure called the Bounded Branch Structure In this branched structure each internal statement branch body is either another bounded branch structure or a sequence in lt Omos gt Or lt Opmos gt OF lt Opbos gt NNIS 3 Bounded Branched Optimization Structure lt Opbos This is a redunda
13. for each of these structures We start with the structurally simplest sequence Consider any non iterative statement sequence consisting of assignments and write statements only We can apply simple transformations 13 to remove all redundant assignments from the sequence The resulting sequences have the property that no variable is assigned twice Hence we have NNIS 1 Minimum Optimization Structure lt Omos gt This is a redundancy free sequence containing assignments and write statements where any variable is assigned only once In EBNF we have lt Omos gt 9 I x E lt Omos gt write E lt Omos gt The order of the statements in a lt Omo gt sequence can be freely interchanged using a straightforward set of substitution rules For example the following two three Statement sequences establish exactly the same postcondition x atb y u v si x y l s atb u v x a b y u v We may extend the complexity of lt Omos gt sequences to include any non iterative statement sequence consisting of assignments and I O statements only When all read statements involve different read variables there exist transformations that allow all read statements to be relocated at the front of the sequence When there exist two read statements involving the same read variable a reassignment rule is used to rename the first read variable and its usages by a fresh variable This allows all read statements to be placed at the front o
14. fy program structure and at the same time make the software more reliable A significant contribution to program structure is made by the statements that change the flow of control the iterative Structures and the selection statements It is the nested composition of such structures which significantly adds to the complexity of programs What we are interested in is a normal form that provides strict guidelines for controlling the complexity of such structures Single point of entry and exit is not strong enough to prevent such structures from becoming rather complex At first sight it would seem that there is not much we can do to reduce the complexity of such structures Proposals to date have concentrated only on normal forms that exploit syntax and as such are not strong enough to control complexity The key lies in proposing normal forms that exploit semantics Semantics allows us to impose more stringent constraints on structures to define forms that are ideal with respect to some clearly specified criterion and identify semantics preserving transformations to convert delinquent structures to normal forms The resulting normal form in each case is not usually a property of a statement per se but of a statement in a specific semantic context In seeking to define normal forms we will use constructive definitions Using this approach to assess whether a given structure is in its normal form it is necessary to carry out a two step proc
15. h BSG to illustrate this u Nsp These quality defects are caused by poor decomposition of the problem We may remove these defects by formally transforming this algorithm into the following equivalent form out Nil do in Nil A ingNil gt if inj headSing head out out iny head iny inq tail in head2iny head out out iny head ing in9 tail fi od do in Nil gt out out in head inj in tail od do inz Nil out out ing head in in tail od The transformations required to achieve this result correspond to splitting the original BSG into its three strongly connected components corresponding to the three loops A more detailed treatment of loop reengineering is given elsewhere 14 3 4 Non Iterative Sequences Simply composing a compound statement of normalized Statements is not strong enough to guarantee that the compound statement is in a normal form Here we consider non iterative sequences that are composed of assignment statements input output statements and if statements There is a potential for un normalized sequences to contain redundant assignments redundant tests and involve the use of variables for more than a single purpose All of these defects may be removed by a sequence of transformations that include several optimizations We will now examine the optimized structures of non iterative statement sequences which contain no logical redundancy An EBNF definition will be given
16. i prex H prec C y C d prex c d prec mod d 5 Normalization of a Program Fragment In this paper we have defined a set of normalization conditions for individual statements and for composite Statements These normal forms which have a mathematical logical basis express an ideal Taken together these requirements provide a basis for constructing what we will call well structured programs Such programs should be composed only of normalized statements at all levels We claim that programs composed only of normalized components are far more likely to be less complex and more reliable To make this point let us consider Manna s Abstract Program AP 10 as an example if p y gt x y do p x gt x f x od O p gt x a if p x do p x gt x f x od 0 p x x f x if p x gt x a do p x gt x f x od fi fi fi When this program fragment is normalized and hence re engineered we get the following equivalent much simpler and non redundant program fragment if p y gt x y O p y gt if p a gt x a sp a gt x f a fi fi 6 Module Normalization Cohesion is usually cited as the criterion that may be used to decide what belongs in a given module and what should be implemented elsewhere 12 Unfortunately this concept is rarely defined precisely enough to be used a basis for module normalization S Two formal requirements must be satisfied for the functionality encapsulated
17. in a module to be cohesive These requirements maybe formulated in terms of input output dependencies Where mutual dependencies exist there is cohesion Assessment of a module s cohesion is easiest to make using a graph theoretic interpretation The two normalization conditions are as follows MVN I1 Each output variable must depend upon at least one input and each input variable must be used to produce at least one output variable MVN 2 The input output variable dependencies must be represented by a single connected bipartite graph The I O dependencies in the diagram below violate this criterion 276 Inputs Outputs If we denote the module input and output sets by I and O and we construct the VDDG graph lt IUO E gt where E is the edge set for the module program then the normalization conditions may be expressed formally as follows MVN 1 V Vxdy xe OnyeI lt x y gt eE MVN 2 VI VO gt I A050 gt 43 lt x y gt E xeI aye O 0 v xeI I aye 0 These two normalization criteria provide a very effective means for deciding what functionality belongs in a particular module In the noncohesive module above the component with output z and dependent inputs d and e should be in a separate module 7 Conclusions Structured programming information hiding and ADTs have made important contributions to program quality However such techniques alone are often not strong enough to control reduce comple
18. ncy free recursively defined sequence that starts with a number of one or more read statements followed by a branch structure in which each branch guard involves at least one read variable assigned by the previous read statements and each internal statement is a sequence in lt O mos OF lt Opmos gt OF lt Opbos lt Opbos gt read x if Cy x gt lt Body gt 0 Cin gt lt Body gt fi read x lt Opbos gt where lt Body gt lt O mos lt Opmos gt lt Opbos gt and where any variable in any lt Oppos gt structure is assigned only once for each execution path and C x for ie 1 m must involve all pre fixed read variables When there exists an if statement whose branch guards are independent of any read variable in the sequence transformations exist which enable us to locate this branch statement at the front of the sequence This constructs a branch structure directly In such a branch structure each internal statement can be simplified into a sequence in lt Oppos gt OF lt Opmos gt OF lt Omos gt NNIS 4 Branch Optimization Structure lt Opgg gt This is a redundancy free branch structure such that all its internal branch statements are sequences in either lt Oppos gt or lt Opmos gt F lt Omos gt lt Opos if Cy gt lt Body gt 0 Cm gt lt Body gt fi where any variable in any lt Opg gt structure is assigned only once for each execution path Sequence
19. of problem Local variables are used to record state information at critical points in a computation It is not easy however to determine the number of local variables for the ideal representation of a given algorithm or program Instead we may use calculations to define the maximum number of local variables to model a particular set of state recording requirements for any algorithm When a program uses more local variables than the maximum required number then its local variable set should be reduced by normalization Before defining the maximum number of local variables needed we need to convert any assignment sequence by substitution into an equivalent multiple assignment x f For example with two output variables x and y the sequence tl x t2 y x t2 y tl produces tl t2 x y x y y x Since x f may contain more local variables than necessary we need to remove the local variable assignments from x f Given any x f and a local variable set J then as long as such a multiple assignment is not bounded by a loop structure we can always achieve x l f where f is the sub set of f after 274 removal of the expression set to which 7 corresponds When x f is in a loop structure not all local variables can be removed e g local variables may depend on their value in a previous iteration The detailed treatment of this is given in 13 After removing local variable assignments either completely or partially
20. of the if statement it must be assigned in every branch of the if statement If this requirement is not fulfilled it leaves open the possibility that on termination of the if statement in some circumstances the variable will be undefined while in other cases it will be defined This represents a correctness problem with the if statement The normalization requirement is designed to avoid this problem NMB 5 While the first normalization condition NMB 1 guarantees that at least one branch is reachable under the deterministic precondition P it does not however guarantee that all branches are reachable under P The normalization condition NMB S5 requires that all branches are reachable under the precondition P NMB 6 To be normalized an overall branch structure must not establish a strongest postcondition that is equivalent to the strongest postcondition established by one or a strict subset of its branches or by a simpler statement S that involves no branches To illustrate NMB 6 let us consider Manna s Abstract Program AP 10 under the precondition true if p y gt x y do ap x gt x f x od 0 p y gt x a if px gt ply ax anp x do p x gt x f x od 0 p x gt x f x p y ax f a a p a if p x gt x a ap y ax an p a ap f a do p x x f x od fi fi fi The last branch statement if p x gt x a do p x gt x f x od fi after execution of its internal statement und
21. s in lt Opgg gt and lt Oppgs gt have similar properties to sequences in lt O mos and lt Opmos gt Each variable is assigned once for each execution path either by a read statement or an assignment and the order of any read statements that bounds a branch structure can be freely changed by appropriate variable substitution within their range Strongest postcondition calculations together with transformations in line provide a means to restructure any non iterative statement sequence into an equivalent optimized redundancy free sequence in lt Omos V lt Opmos gt lt Obbos V lt Opos gt These four structures define the Optimized Structures for any non iterative statement sequence 4 Variable Normalization The way variables are used can have a significant impact on the quality of software Single assignment languages like SISAL overcome most of these problems Here we will consider requirements that may be applied to imperative programs that do not exploit single assignment The consistency principle tells us that a variable should only be used for a single purpose Local variables are frequently used to help achieve this ideal This does not mean however that local variables should be declared freely For example with the module swap x y the ideal segment should use one local variable i e t x x y y t rather than two local variables such as tl x t2 y x t2 y t1 Some formality is needed to resolve this sort
22. t function If sp P G S or sp sp G S a Cj Sj implies one of the branch conditions then other branch conditions cannot be reached Also if either of these conditions implies the negation of a branch condition then that branch is unreachable A normalized branched loop body avoids all of these problems What LBB 2a 2b tell us is that each branched loop should have a strongly connected branch successor graph For example the following List Merge 11 out Nil do in Nil v ing4Nil gt if ing Nil v iny Nil A ing Nil a in headSing head gt out out in head inj inq tail D ing Nil a iny Nil v ing Nil v iny head2iny head out out ing head iny iny tail fi od contains four branches within its loop body if ing Nil out out in head iny iny tail O ing Nil a in Nil gt out out iny head ing ing tail D Ging Nil a iny Nil a inq headSing head gt out out iny head in iny tail O ing Nil a in Nil A in head gt ing head gt out out ing head ing in9 tail fi It satisfies the conditions LBB 1a and LBB 1b however it fails to match LBB 2a and LBB 2b because after execution of the first or second branch the control flow will remain in the same branch or terminate Also after execution of the third branch the control flow will only enter either the second or the third or the fourth branch or terminate and so on We may use the following branch successor grap
23. t it is executable at least twice What this means in formal terms is that the postcondition from the first iteration should not imply the negation of the loop guard LBN 4 Every loop executing under its strongest loop Invariant I should have a structure which guarantees that when the loop body executes it does not establish a condition which implies the loop guard G Obviously if it does the loop is non terminating 3 3 2 Loops with Branched Bodies Loops structures that contain branched bodies are often regarded as the most complex the most difficult to analyze and the most likely to contain logical flaws It is therefore important to see how the concept of normalization may be employed to make such structures more tractable Any loop with a branched body can be transformed into the following equivalent form in many instances S will be empty 14 P do G gt S if C1 gt S1 O C2 gt S2 UET O CN gt SN fi od The basic normalization conditions for loops apply for this loop structure Additional normalization constraints that apply to branch structures are as follows should be reachable i e LBB 1a 3i ie 1 N sp P G S C LBB 1b Ji Gie 1 N sp P G S C After each iteration each branch should be reachable i e LBB 2a Ji Vj i je 1 N sp sp G S a Cj Sj Cj LBB 2b Ji Vj i je 1 N sp sp G S a Cj S C Loop Progress each branch should decrease its varian
24. there are few systematic guiding principles that help us to satisfactorily respond to such questions Clearly it is desirable to have sound and reasoned answers to questions of this sort It is necessary to turn to other related disciplines to find the clues that will help us respond to such questions 0270 5257 96 5 00 1996 IEEE Proceedings of ICSE 18 In abstract algebra 1 logic 8 database theory 16 and other fields normal forms are widely used to settle issues of structure to define ideals of form and to provide efficiencies and economies of expression In contrast in computing there has been little interest in employing normal forms The tremendous advantages that have been gained from using normal forms in related fields suggests that it might be well worth our while to try to develop a normal form theory for program structures Existing structuring proposals have not done enough to control complexity and improve the reliability and overall quality of software The fact that program structures can be modelled using graph theory and that the semantics of program statements may be modelled as predicate transformers 2 4 13 provides an excellent opportunity to search for normal forms that may capture ideals of form and composition that can point the way to the construction of software that is simpler more reliable more efficient and easier to maintain We will also show that such techniques offer an excellent opportunity to p
25. ut measurement of the relative quality of software and its complexity on a much sounder mathematical footing In putting forward proposals for the use of normal forms in programming we are not interested in projecting the theory of program structure into an obscure realm of abstract mathematics What we are interested in doing is providing sound mathematically grounded practical principles that can be routinely used by software engineers to guide the construction and measurement of key properties of software that impact its quality These principles define ideals of form according to clearly enunciated criteria and therefore also open up the possibility of re engineering poor quality software to a normal form What we will put forward here is one set of proposals for normal forms There may certainly be other alternatives It is our hope that the present work will encourage others to look at the structure of software from this perspective 2 Normal Forms and Program Structure In applying the concept of normal forms to program Structure there are three possible avenues of exploration that we can pursue We can start by looking at possible normal forms for simple and composite statements and statement components This avenue also takes into account a number of issues of composition Another fruitful place to look is at modules There have been proposals by Myers and others relating to coupling and cohesion 12 These proposals like the pr
26. v x 140A flag PQx Da x eoflag a x 1v x 1 P x la x 1 flag From a logical viewpoint the flag is equivalent to the predicate x 1 which means there is redundancy present 271 From a programming viewpoint when the flag is needed in the preceding program the predicate x 1 may be used to replace it In contrast if Afi 1 lt A p gt i i 1 Af i 1 gt A p gt i p i 1 i 1 fi is a normalized branch statement under the precondition Spe 1 i Vte 1 p 1 Vse p 1 i A t lt A pJAA s lt A p because sp Spe 1 i Vte 1 p 1 Vse p 1 i A t lt A p AA s lt A p if Ali 1 lt A p gt i i 1 Ali 1 gt Alp gt i p i 1 i 1 fi Ape 1 i Vte 1 p 1 Vse p 1 iJA t lt A p AA s SA p v Vte 1 i 1JA t lt A iJAp i Spe 1 i Vte 1 p 1 Vse p 1 iJA t lt A p AA s SA p as the latter implies the former 3 3 Loops The use of semantics allows us to clearly and precisely define a number of important structural and correctness requirements for loops We will divide our discussion of the normalization requirements into two parts the first part consists of requirements that apply to all loops and the second consists of those requirements that apply to loops that contain branched loop bodies i e they contain IF statements and or loops In our discussion we will consider a general loop do G S od that executes under a precondition P These requirements extend beyond the usual requirements for loop correctness 4
27. wing conditions must be satisfied in concert P gt CyvCgv vCn Vi ie 1 N P D A variable unassigned in P that is assigned in at least one branch must be assigned in all branches i Ge 1 N P C a di ie 1 N P C Ji sp PAC S1 v v sp PACN Sy sp P S sp PAC S4 v v sp PACy SN is conjunctive NMB 1 The first normalization condition ensures that the if statement is able to accommodate all possible initial states under which it is required to execute That is there will be no initial state defined by P for which all branch guards are false NMB 2 For reasons of efficiency and consistency it is desirable that for any given precondition the guard for only one branch should be satisfied What this means in formal terms is that for all branch guards the satisfaction of any guard means that all other branch guards are not satisfied The second normalization condition NMB 2 captures this requirement NMB 3 A non empty branch statement Cj gt Sj Dj in an if statement is redundant when that statement establishes a 270 postcondition Dj that is equivalent to the precondition P for the if statement A normalized if statement should contain no redundant branches NMB 4 A significant insecurity in if statements in most languages is that they do not enforce the requirement that a variable which is unassigned in the precondition P and is assigned in at least one branch
28. xity to manageable levels make software more reliable and make it easier to understand and change The weakness of these methods when they are applied to structures is that they do not effectively take into account contextual and semantic issues As a result they do not guarantee that complexity will be limited and that high quality software will always be produced by following their guidelines What we have suggested in the present discussion is that there exists beyond structured programming another level of structuring based on context and semantics This level is more subtle but it is significant in its impact on the quality of software In the past decades much of the mathematics formal methods that have been brought to bear on programs has looked only at the semantics correctness of components What we need to invent is the mathematics logic of structure for program components composed and uncomposed Normalization of simple and complex statements of variable usage and of modules provides a vehicle for achieving these goals To realize the normal forms we have described we have three choices get the programming language to enforce them leave it to users to design components that conform to the normal form requirements or develop tools that can automatically re engineer un normalized components to their corresponding normal forms Obviously the first choice is the best It does however require some refinements to existing l
Download Pdf Manuals
Related Search