SOFTWARE TESTVERIFI CEN 6070
Popular in Course
Popular in Computer Engineering
This 181 page Class Notes was uploaded by Paxton Okuneva on Saturday September 19, 2015. The Class Notes belongs to CEN 6070 at University of Florida taught by Stephen Thebaut in Fall. Since its upload, it has received 16 views. For similar materials see /class/207040/cen-6070-university-of-florida in Computer Engineering at University of Florida.
Reviews for SOFTWARE TESTVERIFI
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/19/15
Lecture 24 Prepared by Stephen M Thebaut PhD University of Florida Iteration Recursion Lemma IRL Correctness conditions for whileido statement Sufficient correctness conditions Correctness conditions for repeatiuntil statement Invariant Status Theorem While Loop Initialization In Lecture 18 we learned that synthesizing a loop invariant is a trial and error process We now consider a way to systematically derive loop invariants when the function computed by the loop is known Consider the following assertion where 20 and y0 represent the initial values of z and y respectively true while zltgt0 do y y1 z 2 1 endiwhile z0 A yyo20 Can you identify an invariant I that could be used to prove this 4 true while zltgt0 do y y1 z 2 1 endiwhile z0 A yyo20 Now what function f is computed by the loop Where fis defined what is fVX What is fVXO What do we get if we set fVX equal to fVXO 4 true while zltgt0 do y yl y yo20z z 2 1 endiwhile Consider I This can be rewritten as 20 A yy0zo YZ Yozo So 1 220 a zy 0yz and setting fVX equal to fVXO gives yz y0zoie1 Finally what is the relationship between fand the specified postcondition true while zltgt0 do y yl y yo20z Z Z1 This can be rewritten as endiwhile Consider 1 20 A yy0zo YZ YoZo So 1 220 a zy 0yz and setting fVX equal to fVXO gives yz y0zoie1 Finally what is the relationship between fand the specified postcondition zfZXO A yfvXO This can be written more simply as just XfX0 Theorem Let f while p do g If X06 Df XE Df and qX fXfXo then q is an invariant of while p do 9 and has the following properties 1 qX0 is true and 2 qXpX 2 qogX and 3 qX A pX 2 XfXo Proof qX0 is true 11X fXfXo SO QXo fXofXo true as desired Proof cont d 2 qX A pX 2 qogX For X6 Df we know p X 2 fX fogX by the Correctness Theorem Since qXfXfXo by definition it follows that qX DX 2 fogXfXo Proof cont d But the right hand side of 11X A pX 2 fogXfXo is just fgXfXo qgX qogX Therefore qX A pX 2 qog X as desired Proof cont d 3 11X A pX 2 XfXo If upX then fX I by de nition of the while construct This can be rewritten as fX X Since 11X fXfXo it follows that pX A qX 2 XfXo as desired Consider the following assertion where 20 and y0 represent the initial values of z and y respectively true while 2lt gt0 do y y1 z 2 1 endiwhile 20 A yyo20 Consider the following assertion where 20 and y0 represent the initial values of z and y respectively true What function 1 while 2lt gt0 do is computed by y y1 the while loop 2 2 1 endiwhile 20 A yyo20 For f 220 a zy 0yz an invariant fXfX0 can be derived by tabulating fX and fXo for each member of the data space X X fX fXo 2 Y and equating components of fX and fXo For f 220 a zy 0yz an invariant fXfX0 can be derived by tabulating fX and fXo for each member of the data space X X fX fXo z 0 0 Y YZ Y0Zo and equating components of fX and fXo For f 220 a zy 0yz an invariant fXfX0 can be derived by tabulating fX and fXo for each member of the data space X X fX fXo z 0 0 Y YZ Y0Zo and equating components of fX and fXo 0 o yZ y020 We can rewrite the second equation as Y Yo i39zoZ and use it as an invariant to prove the given assertion using the while loop rule of inference Try it out In many situations a loop invariant may hold by virtue of its initialization In particular given f while p do 9 X0 6 Df a limited invariant of the initialized while loop h while p do 9 11X fXf0hXo is Such an invariant has the following properties 1 qohX0 is true and 2 qXpX 2 qogX and 3 11X 39pX 3 Xf0hXo Consider the assertion while kltgtn do p 1 2p k k1 endiwhile p2quot Consider the assertion What function h is computed by the loop initialization while kltgtn do p 1 2p k k1 endiwhile p2quot Consider the assertion while kltgtn do p 2p What function f k k1 is computed by endiwhile the while loop p2quot For f kSn a pk p2quot39kn and h pk 10 an invariant fXfohX0 can be derived by tabulating fX and fohX0 for each member of the data Space X fX fohX0 p k and equating components of fX and foh X0 I These equations combine to yield the invariant p 2k which can be used to prove the given assertion using the while loop rule of inference Recall that in Example 3 of Lecture 18 we proved the assertion below using the invariant I ZXJ true Z X J 1 while JltgtY do Z ZX J J1 endiwhile ZXY Derive a limited invariant for the initialized while loop using the Invariant Status Theorem Invariant Status Theorem While Loop Initialization Lecture 24 Prepared by Stephen M Thebaut PhD University of Florida Requirements and Specifications Software Testing and Verification Lecture 3 Prepared by Stephen M Thebout PhD University of Florida thi are Requirements and Specifications Requirement something required something wanted or needed an essential requisite To Specify to name to state explicitly or in sufficient detail Roles of Requirements in Testing and Verification How are requirements used in testing Serve as basis for blackbox test case design Source of expected results for ALL test cases What do requirements have to do with the formal correctness assertions PisiQ fSJ What if there are no requirements Roles of Requirements in Testing and Verification conl d Bottom Line testing and veri cation only make sense when requirements in some form are available to work with Exercise Consider the following pseudocode program Sum 0 1 while JltN do Sum Sum XJ J Jl endiwhile What does it do Is it correct Requirements Types Functional versus Non Functional Formal versus Informal Structured versus Unstructured State model based versus Operational Graphical versus Textual A Sampling of Requirement Representations Natural language prose Numbered paragraphs ala DoD standards Functions Attributes and Constraints ala Gause amp Weinberg Structured templates of various sorts and levels Decision tables Pseudocode programs A Sampling of Requirement Representations cont d PDL models PSL RSL etc Cause Effect models State Transition models Pre and Post conditions Recursive Function definitions Algebraic specifications Z based Schemas Etc Requirements Sources at Different Levels Typical System Level Sources Objectives document User manuals eg MAN Pagesquot Installation documents Service manuals Requirements de nitionspeci cation Requirements Sources at Different Levels cont d Typical Unit Level Sources Modulefunctionprocedure specifications Pseudocode Logic specifications Object classmethod specifications Requirements Sources at Different Levels conl d Typical Intermediate eg Product Component Level Sources Productcomponent specification Functional speci cation Object use include relations sequencecollaboration diagrams package speci cation Some Key Attributes Completeness Consistency Unambiguousness Veri abilityTestability Correctness Completeness Possible De nition for Functional Requirements The desired response is specified for every possible stimulus and every system state Definition for Non Functional Requirements Constraints and preferences for every relevant attribute of every desired function are speci ed Consistency Possible De nition There are no contradictions or conflicts in any speci ed functional or non functional requirements Unambiguousness Possible De nition Requirements are not subject to multiple interpretations Gause amp Weinberg s heuristics for identifying potential ambiguity Mary Had a Little Lamb emphasize different words Mary Conned the Trader substitute synonyms 39 had a r a little lamb little lamb Mary had a little lamb Mary had a Mary had a l little quot Mary owned a Mary consumed a small petite lamb amount of lamb Mary had a little lamb Mary was involved Mary conned with a young sheep the trader and VerifiabililyTeslabilily Possible De nition Objective criteria exist for determining whether or not requirements will have been satisfied What about CORRECTN ESS The notion ofa PROGRAM being correct with respect to its requirements is relatively straightforward but what does it mean to say that a program s REQUIREMENTS are correct a commim Damages jam m og m nmEu a u A J y a ammumnw x anc oBmznm o n APE Umm j no1 D WW4 What about CORRECTNESS conl d In other words the correctness of a requirements speci cation would be considered with respect to a design that incorporates that speci cation For example you might ask Was the decision to take this course correct with respect to my overall plan of study What about CORRECTNESS conl d Based on our definition the answer would be yes if your plan of study a design that incorporates this course satisfies your educational goals ie the requirements for your plan What role canshould testers play in assessingverifying the degree to which requirements are complete consistent unambiguous verifiable correct Requirements and Specifications Software Testing and Verification Lecture 3 Prepared by Stephen M Thebout PhD University of Florida WhiteBox Testing Techniques Software Testing and Verification Lecture 7 Prepared by Stephen M Thebout PhD University of Florida Testing based on analysis internal logic design code etc But expected results still come from requirements quot Also know as structural testing White box testing concerns techniques for designing tests it is not a level 0 ting White box testing techniques apan primariiy to lower levels of testing eg unit and component WhiteBox Testing Topics Logic coverage lecture I Data ow coverage lecture 11 Path conditions and symbolic execution lecture 111 Other white box testing strategies eg fault based testing lecture IV Types of Logic Coverage Statement each statement executed at least once Branch each branch traversed and every entry point taken at least once Condition each condition True at least once and False at least once BranchCondition both Branch and Condition coverage achieved Types of Logic Coverage cont d Compound Condition all combinations of condition values at every branch statement covered and every entry point ta ken Path all program paths traversed at least once Pseudocode and Control Flow Graphs inputY if Ylt0 then Y Y endiif while Ygt0 do inputX Y Y1 endiwhile Statement Coverage Statement Coverage requires that each statement will have been executed at least once Simplest form of logic coverage Also known as Node Coverage What is the minimum number of test cases required to achieve statement coverage for the program segment given below Minimum Required for Statement Coverage inputY if Ylt0 then Y Y endiif while Ygt0 do inputX Y Y1 endiwhile Branch Coverage Branch Coverage requires that each branch will have been traversed and that every program entry point will have been taken at least once Also known as Edge Coverage Branch Coverage cont39d Why and that every program entry point will have been taken at least once Branch Coverage cont39d Why and that every program entry point will have been taken at least once Branch Coverage cont39d What is the relationship between Statement and Branch Coverage Branch Coverage cont39d What is the relationship between Statement and Branch Coverage Possible relationships None Statement Coverage subsumes Branch Coverage statement gt branch Branch Coverage subsumes Statement Coverage branch gt statement statement gt branchquot Min number of cases required for Statement Coverage Min number of cases required for Branch Coverage branch gt statementquot branch gt statementquot Normally YES But not in the presence of DEAD CODE DEAD CODE is not reachable via any executable program path a Condition Coverage A branch predicate may have more than one condition inputXY if Ylt 0 or X0 then Y Y endiif while Ygt0 and not EOF do inputX Y Y1 endiwhile Condition Coverage cont39d Condition Coverage requires that each condition will have been True at least once and False at least once What is the relationship between Branch 7 and Condition Coverage Condition Coverage cont39d 39fA Bth lslor en A B Branch else test1 T F true 52 endiifithenielse teStZ F F false Condition Coverage cont39d 39fA Bth lslor en A B Branch else test3 T F true 52 endiifithenielse teSt4 F T true BranchCondition Coverage BranchCondition Coverage requires that both Branch AND Condition Coverage will have been achieved Therefore BranchCondition Coverage subsumes both Branch Coverage and Condition Coverage Compound Condition Coverage What if the compiler generates code that masks the evaluation of conditions That is suppose if A or yx5 then is compiled in such a way that ifA is true yx5 will not be evaluated Also know as Multiple Condition Coverage Subsumes BranchCondition Coverage regardless of the order in which conditions are evaluated Compound Condition Coverage cont39d Combinations of condition values TT TF FT FF inputXY if Ylt 0 or X0 then Y Y endiif Compound Condition Coverage cont39d In general how many different combinations of condition values must be considered when a branch predicate has N conditions quot Olten described as the strongest coverage Is it stronger than Compoun Condition Coverage Path Coverage is usually impossible when loops are present How many test cases would be required to cover all paths in the example below A Path Coverage C quott39d forI lt03Odo inputXY 0 then if Xlt0 then Y X else endjor7d0 Path Coverage cont39d 3 paths 3 paths Path Coverage cont39d Path Coverage cont39d Various strategies have been developed for identifying useful subsets of paths for testing when Path Coverage is impractical Loop Coverage Basis Paths Coverage and Dataflow Coverage Loop Coverage Loop Coverage requires that the body of loops be executed 0 1 2 t max and max1 times where possible Rationale 0 Is some action taken in the body that must also be taken when the body is not executed 1 Check lower bound on number of times body may be executed Loop Coverage cont39d Rationale cont d 2 Check loop re initialization t Check typical number of iterations max Check upper valid bound on number of times body may e executed max1 If the maximum can be exceeded what behavior results Basis Paths Coverage A coverage criterion associated with McCabe s Structured Testing Based on idea of identifying a spanning ie basis set of paths for a program s equot path spac The number C of such paths is equal to the number of 2 way branch statements in the program 1 This is also the number of enclosed regions in the program graph 1 sad a C is what McCabe calls the Cyciomari Compexiiy of a program Example 1 if a then s1 else if b then s2 else if c then s3 else s4 endiifithenielse endiifithenielse endiifithenielse Paths Basis Paths Cases for branch coverage i sad Example 2 if a then 51 endiifithen if b then 52 endiifithen if c then 53 endiifithen Paths Basis Paths Cases for branch coverage if A Example 3 while a do if b then 51 else 52 endiifithenielse endiwhile Paths Basis Paths Cases for branch coverage i d In General Number of Number of CNausngsber ogitzztfor program Paths 2 Basis Paths 2 q branch coverage Basis Paths Path Coverage gt Coverage gt Branch Coverage and Exercise Prove that Path and Compound Condition Coverage are independent Hint consider the proof that Branch and Condition Coverage are independent Summary of WhiteBox Coverage Relationships so far Compound Condition 1 Branch Cendition BaSIS Paths Condition Statement Coming Up Next In the next lecture we consider a family of path selection criteria based on the idea that program paths along which variables are de ned and then used should be covered The strategy is popularly known as Dataflow Coverage WhiteBox Testing Techniques Software Testing and Verification Lecture 7 Prepared by Stephen M Thebout PhD University of Florida Formal Program Specification Software Testing and Veri cation Lecture 16 Prepared by Stephen M Thebout PhD University of Florida Overview Review of Basics Propositions propositional logic predicates predicate calculus Sets Relations and Functions Speci cation via pre and post conditions Speci cations via functions Propositions and Proposilionol Logic A proposition P is a statement of some alleged fact which must be either true or false and not both Which of the following are propositions elephants are mammals France is in Asia go away 5 gt 4 X gt 5 Propositional Logic is a formal language that allows us to reason about propositions The alphabet of this language is P Q R A V gt ltgt where P Q R are propositions and the other symbols usually referred to as connectives provide ways in which compound propositions can be built from simpler ones Trulh Tables Truth tables provide a concise way of giving the meaning of compound forms in a tabular form Example construct a truth table to show all possible interpretation for the following sentences AVBABondAltB Equivalence Two sentences are said to be equivalent if and only if their truth values are the same under every interpretation If A is equivalent to B we write A E B Exercise Use a truth table to show PQQV P Equivalence conl d Many users of logic slip into the habit of using lt2 and E interchangeably However AltB is written down in the full knowledge that it may denote either true or false in some interpretation whereas AEB is an expression of fact ie the writer thinks it is true Predicates Predicates are expressions containing one or more free variables place holders that can be lled by suitable objects to create propositions For example instantiating the value 2 for X in the predicate Xgt5 results in the false proposition 2gt5 Predicales conl d Note that a predicate itself has no truth value it expresses a property or relation using variables Predicales conl d There are TWO ways in which predicates can give rise to propositions As illustrated above their free variables may be instantiated with the names of speci c objects an They may be quantified Quanti cation introduces two additional symbols V and 3 Predicales conl d 0 V and 3 are used to represent universal and existential quantification respectively VX o duckx represents the proposition every object is a duck 3X 0 duckx represents the proposition there is at least one uck Predicaies coni d For a predicate with two free variables quantifying over one of them yields another predicate with one free variable as in vx o Qxy or EIX o QXy Predicales conl d Where appropriate a domain of interest may be speci ed which contains the objects for which the quanti er applies For example Vi fl2Nl 0 Aigt0 represents the predicate the first N elements of array A are all greater than 0 Predicate Calculus The addition of a deductive apparatus gives us a formal system permitting proofs and derivations which we will refer to as the predicate calculus The system is based on providing rules of inference for introducing an removing each of the ve connective symbols plus the two quanti ers Predicate Calculus coni d A rule of inference is expressed in the form AVA n C and is interpreted to mean AWAAQAAAngtC Predicate Calculus cont d Examples of deductive rules AA B A A Predicate Calculus cont d Examples of deductive rules cont d AltB ABBA AQB AltgtB VX o PX Pm A PnQ A A Pnk Sets and Relations A set is any well defined collection of objects called members or elements The relation of membership between a member m and a set S is written m S If m is not a member of S we write m S o A reiation r is a set whose members if any are all ordered pairs quot The set composed of the first member of each pair is called the domain of r and is denoted Dr Members of Dr are called argun aents of r 0 The set composed of the second member of each pair is called the range of r and is denoted Rr Members of Rr are called values of r Functions A function f is a relation such that for each X Df there exists a unique element Xy f We often express this as y fx where y is the unique value corresponding to x in the function f It is the uniqueness of y that distinguishes a function from other relations Functions coni d It is olten convenient to define a function by giving its domain and a rule for calculating the corresponding value for each argument in the domain For example f Xy Ix Oiy x2 3x 2 This could also be written fX X2 3X 2 where Df0i Conditional Rules Conditional rules are a sequence of predicate a rule pairs separated by vertical bars and enclosed in parentheses plarllpzarZIHkaark Conditional Rules conl d The meaning is evaluate predicates p1 p2pllt in order for the first predicate pi which evaluates to true it any use the rule ri if no predicate evaluates to true the rule is unde ned Note that a 4 2 Conditional Rules conl d For example f Xy X divisible by 2 gt y X2 X divisible by 3 gt y X3 true gt y X Note that true a r has the effect of if all else fails use r Recursive Functions A recursive function is a function that is de ned by using the function itself in the rule that defines it For example oddevenX X Oi gt X Xgt i gt oddevenX2 X lt O gt oddevenX2 Exercise de ne the factorial function recursively Specification vio Pre and Post Conditions The functional requirements of a program may be speci ed by providing an explicit predicate on its state before execution a pre condition an an explicit predicate on its state aiter execution a post condition Specification via Pre and Post Condiiions coni d Describing the state transition in two parts highlights the distinction between the assumptions that an implementer is allowed to make an the obligation that must be met Specification via Pre and Post Condiiions coni d The language of pre and post conditions is that of the predicate calculus Predicates denote properties of program variables or relations between them Example 1 Consider the pre and post conditions for a program that sets variable MAX to the maximum value of two integers A and B pre condition post condition Example 2 Consider the pre and post conditions for a program that sets variable MIN to the minimum value in the unsorted non empty array A1N pre condition post condition What does unsorted mean here Example 2 coni d Possible interpretations of unsorted 1 Vi fi2Ni o Ai90ii V ViH2Ni o Ai2Aii 2 the sort operation has not been applied to A What was the speci er s intent Specification via Functions Programs may also be speci ed via the use of an assignment function The domain of the function corresponds to the initial data states that are transformed into final data states by the program Specification via Functions coni d For example in a program with data space x y z the assignment statement X y corresponds to a set of ordered pairs of the form Initial flna X y Z Y y z Specification via Functions coni d 7 Likewise the functio 1l fX20y20axyxy0 speci es a program for which the nal value of x is the sum of the initial values of x and y an the nal value of y is 0 ifx and y are both initially 2 0 Otherwise the program does not terminate since f is not de ned in this case A Formal Program Specification Software Testing and Veri cation Lecture 16 Prepared by Stephen M Thebout PhD University of Florida Exercise Solutions Functional Verification Software Testing and Veri cation Prepared by Stephen M Thebaut PhD University of Florida Exercise Identity function Given XIV X P if xgty then xy yx f1 xgty a xy yx true a1 f2 xgty a xy yx xlty a1 1 3 Xiy a xy M Fill in the following correctness table I CComplete SSufficient N Neither Exercise Identity function Given XIV X P if xgty then xy yx f1 xgty a xy yx true a1 f2 xgty a xy yx xlty a1 1 3 Xiy a xy M Fill in the following correctness table CComplete SSufficient N Neither Exercise I Prove f P where f X17 a xy 1720 true a xy x x and P is if x 17 then x3 y endiifielse ifihenelse Correctness Conditions Complete correctness conditions for f if p then G else H where g G and h H have been shown Prove p 2 f g A p 2 f h Working correctness questions When p is true does fequal g When p is false does fequal h Proof that f P f x17 a xy 1720 true a xy x x P if x 17 then y x3 else y x endiifielse Proof that f P f x17 a xy 1720 true a xy x x P if x17 then y x3 G else y x endiifielse By observation 9 xy xx3 h xy x x Proof that f P coni d Therefore by the Axiom of Replacement it is sufficient to show f x17 a xy 1720 true a xy x x ifp then xy xx3 else xy x x 7 g I When p is true does fequal g x17 2 f xy 1720 x17 2 g xy xx3 gt xy 1720 When p is false does fequal h x 17 2 f xy x x gt v x 17 2 h xy x x Exercise For program P below where all variables are integers hypothesize a function ffor P and prove f P while iltn do t tx i i 1 endiwhile Exercise For program P below where all variables are integers hypothesize a function ffor P and prove f P while iltn do t tx i i 1 endiwhile Hypothesized f iltn a it ntxquot39i iZn a1 Alternative f iSn a it ntxquot39i igtn a 1 Does it make any difference which we use d whiledo Correctness Conditions Complete correctness conditions for f while p do 9 where g G has been shown Prove termfP A p 2 f fo 9 A p 2 f I whiledo Correctness Conditions coni d Working correctness questions Is loop termination guaranteed for any argument of f When p is true does fequal f composed with 9 When p is false does fequal Identity Proof that f P f iltn gt it ntxquot39i i2n gt I P while iltn do t tx i i1 endwhie Proof that f P f iltn gt it ntxquot39i i2n gt I p P while Iltn do t tx G i i1 endwhie By observation 9 G it i1tx Is loop termination guaranteed for any argument of f Show this using the Method of Well Founded Sets Proof that f P cont d Does i2nf1 Proof that f P conl d Doesi2nf1 Does iltnf fog iltn 2 f it ntx 39i iltn 2 fo 9 fo it i1tx What is fwhen applied alter 9 changes the initial value of i Recall f iltn gt it ntxquot i i2n gt I There are two cases to consider in 1 amp iltn 1 ai Proof that f P cont d Does iltnffog iltn 2 f it ntx 39i iltn 2 fo 9 fo it i1tx case a in 1fo g I o it i1tX I o it n11tx I o it ntx1 I o it mm it ntx 39i N 4 Proof that f P cont d Does iltnf fog iltn 2 f it ntx 39i iltn 2 fo 9 fo it i1tx case b iltn 1fo g it mm o it i1tx it ntxx 39i1 it ntxx 39i391 it ntx 39i3911 it ntX 39i fx Exercise For program R below where all variables are integers hypothesize a function r for R and prove r R repeat x x 1 y y2 until x0 Exercise For program R below where all variables are integers hypothesize a function r for R and prove r R repeat x x 1 y y2 until x0 Hypothesized r xgt0 a xy 0y2X repeoLuniil Correctness Conditions Complete correctness conditions for f P repeat 9 until p where g G has been shown Prove termfP A p09fgl pog 0 fog Proof that r R r Xgt0 gt Xy 0y2x R repeat x x 1 y y2 G until x0 p By observation 9 G Xy X1y2 ad Proof that r R r Xgt0 gt Xy 0y2x R repeat x x 1 y y2 G until x0 p By observation 9 G Xy X1y2 Is loop termination guaranteed for any argument of r Show this using the Method of Well Founded Sets Proof that f P cont d Doespogrg Recall r Xgt0 gt Xy 0y2x ad Proof that f P cont d Does pogrg X0 o xy x1y2 2 x01 x1 2 r xy 0y2x xy 0y2 x1 2 g xy x 1y2gt v xy 0y2 Recall r Xgt0 gt Xy 0y2x ai Proof that f P cont d Does pogrrog Recall r xgt0 a xy 0y2x ad Proof that f P cont d Does upog r rog x0 o xy XLY2 13Xoil Thus there are 2 cases to consider X0lt 1 and x0gt1 case a xlt 1 2 r undefined xlt1 2 rog unde unde ned since uxgt0 o gxlt 1 Recall r xgt0 a xy 0y2x Proof that f P cont d case b xgt1 r xy 0y2x xgt1 r0 9 xy 0y2x o xy x 1y2 since xgt0 o gxgt1 le 1 0y22x 1 XIY l 0y22x 2 xy 1 01Y2X Therefore p o g 2 r r o g Recall r xgt0 a xy 0y2x ai Exercise Derive a limited invariant for the initialized while loop using the Invariant Status Theorem true Z X J 1 while JltgtY do Z ZX J J1 endiwhile ZXY Exercise Derive a limited invariant for the initialized while loop using the Invariant Status Theorem What function h is computed by the loop initialization 2 X1 What function f is computed by the while loop true Z X J 1 while JltgtY do Z ZX J J1 endiwhile ZXY JSY a ZJX ZXY JYX ai For f JSY a ZJX ZXY JYX and h ZJ X1 an invariant fXfohX0 can be derived by tabulating fX and fohX0 for each member of the data space X fX fohxo Z ZXYJ XOXOYD1 J Y Yo x x m and equating components of fX and fohX0 zmwnxwxgm4 Y m Xm equating foo and fohXo ZXY J X0X0Y01 Y 0 XX0 ZXY J XXY 1 z XXY 1 XY J J Recall that in Example 3 of Lecture 18 we proved the given assertion using this invariant ad Predicate Transforms Software Testing and Veri cation Lecture 20 Prepared by Stephen M Thebout PhD University of Florida Predicate Transforms and II Introduction Proving strong correctness Assignment statements Sequencing Selection statements Iteration Rule for whiledo Statement In order for the program while b do S to terminate in state Q it is necessary that 0 b is initially false and Q holds OR 1 b is initially true and alter executing S b and Q hold OR b is initially true and alter executing S b is still true and after executing S a second time b and Q hold OR Rule for whiledo Statement cont d Thus we can write wpwhile b do S Q E HOV H1 V H2 V where H0 2 b A Q H1 2 b A wpS b A Q H2 2 b A wpS b A wpS b A Q Rule for whiledo Statement cont d Equivalently we can write wpwhie b do S Q E Ha V H1 V H2 V where H0 2 b A Q H1 2 b A wps H0 H2 2 b A wps H1 Hi 3 b A IWPS Hr1 Something to think about How do these terms compare to the infinite set of necessary conditions derived for the whileido ROI What is the relationship between wpwhie b do S Q and an invariant I for which initialization preservation and finalization hold Example For what initial values of i n and t will the following program terminate with txquot while i lt n do t tx i i1 endiwhile How about i1 n2 and t1 Can you think of any others Example conl d Find the wp of this program with respect to the post condition txquot Attempt to find a regularity in terms that allows a closed form expression Example cont d HOE bAQ H while i lt n do igtnAtxquot FlltX t A Wps H n emljvThliile1 ISn A wpS gtn Atx iSn A i1gtn Atxxquot in Atxquot391 b A wpS H1 isn A wpS in Atxquot391 iSn A i1n Atxxquot391 in 1 txquot392 Example cont d H3 3 b A wpS H2 while i lt n do isn A wpSin1 Atxquot392 t tx isnAi1n 1Atxxquot392 I i in2 AtXn3 endiwhlle b A wpS Hm in k 1Atxquot39k in k1 Atxquot39k Example cont d Thus we have Ha igtn Atxquot Hk in k1 Atxquot39k for all kgt0 iSn A txi391 since in k1 2 n ki 1 Therefore wp E H0 V H1 V H2 V igtn Atxquot V iSn Atxi391 Example conl d So given that the wp is igtn Atxquot v iSn Atxi391 which of the following initial states will result in the program terminating with txquot i1 A t1 A n21 i3 A tx A n1 i2 A tx A n5 Loop Invariants and wp s In general will loops terminate when P 2 wp For while loops does wp A b S wp Does wp A b 2 Q wp E weakest loop invariant which guarantees termination Predicate Transforms Software Testing and Veri cation Lecture 20 Prepared by Stephen M Thebout PhD University of Florida Cleanroom Software Engineering Software Testing and Veri cation Lecture 25 Prepared by Stephen M Thebout PhD University of Florida 5 Required Reading Linger Cleanroom Software Engineering for ZeroDefect Software Proceedings 15th Int Conf on Solt Eng 1993 IEEE Computer Society Press pp 2 13 Cr Additional relevant reference Linger Trammell Cleanroom Software Engineering Reference Model CMUSEI 96 TR 022 Software Engineering Institute 1996
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'