SOFTWARE TESTVERIFI CEN 6070
Popular in Course
Popular in Computer Engineering
This 26 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 9 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
Functional Verification Software Testing and Veri cation Lecture 2 1 Prepared by Stephen M Thebaut PhD University of Florida Overview of Topics 1 Introduction 2 Verifying correctness in program reading writing and validation 3 Complete and sufficient correctness 4 Compound programs and the Axiom of Replacement Introduction What is functional veri cation A function theoretic based approach for determining the correctness of structured programs Correctness is de ned as a correspondence between a program and its intended function Reference Linger Mills ampWitt Structured Programming Theory and Practice AddisonWesley 1979 Tasks in Program Reading Writing and Verification Tasks encountered in reading writing and verifying programs are identical Program Reading Abstract a given program construct eg an ifithen else statement into a hypothesized function f The task is to show f if p then G else H Tasks in Program Reading Writing and Verification cont d Program Writing Expand a given function finto a hypothesized program construct eg an ifithenielse statement The task is to show f if p then G else H Tasks in Program Reading Writing and Verification cont d Program Verification Given both function fand its hypothesized program expansion eg an ifithen else statement the task is to show f if p then G else H Tasks in Program Reading Writing and Verification cont d In all three cases we seek to confirm the equivalence or subset relationship of two expressions each representing the function of a program Complete and Sufficient Correctness Given a function fand a program P claimed to implement f correctness is concerned with one of two questions Is f P Is fequivalent to the function computed by P question of complete correctness Is fc P Is fa subset of the function computed by P A question of suf cient correctness Complete and Sufficient Correctness conl d In the case of complete correctness P computes values for arguments in Df only P is unde ned for arguments outside Df In the case of suf cient correctness P may compute values from arguments not in Df Note that by de nition f P implies fc P Correctness Relations Example 1 For integers xy consider the function f y20 a xy xy0 and the programs P while ygt0 do xy x1y 1 P while ylt gt0 do xy x1y 1 Example I cont d Consider P1 while ygt0 do xy x1y 1 ygt0 a y0 a ylt0 a f y20 a xy xy0 Example I cont d Consider P2 while ylt gt0 do xy x1y 1 ygt0 a y0 a ylt0 a f y20 a xy xy0 Example I cont d Both programs satisfy suf cient correctness Both correctly compute fxy for y20 Only P2 satis es complete correctness P1 terminates for negative y Handling Invalid Inputs fcan be redefined to handle invalid inputs 1quot y20 a xy2 Xy0z true a xyz xy error Consider P3 below Does f P3 P3 if ylt0 then 2 error e se while ygt0 do xy x1y 1 Example 2 Given P while xgt0 do xy x 1y2 while xlt gt0 do xy x 1y2 xgt0 a xy 0y2x x20 a xy 0y2x Fill in the following correctness table P1 P2 CComplete and Sufficient SSufficient only N Neither Example 2 cont d Consider P1 while xgt0 do xy 1 X391IY2 Xgt0 a X0 a Xlt0a f1 xgt0 a xy l 01Y2X f2 x20 a xy 0Y2X Example 2 coni d Given while xgt0 do xy x 1y2 while xlt gt0 do xy x 1y2 xgt0 a xy 0y2x x20 a xy 0y2x Fill in the following table CComplete and Sufficient SSufficient only NNeither Example 2 cont d Consider P2 while xlt gt0 do xy x 1y2 Xgt0 a X0 a Xlt0a f1 xgt0 a xy 0y2x f2 x20 a xy 0y2x Example 2 coni d Given while xgt0 do xy x 1y2 while xlt gt0 do xy x 1y2 xgt0 a xy 0y2x x20 a xy 0y2x Fill in the following table 2 CComplete and Sufficient P1 P f1 SSufficient only G N Neither Exercise Identify function Given XIV X P ifxgty then xy yx f1 xgty a xy yx true a1 f2 xgty a xy yx xlty a1 f3 Xiy a xy M Fill in the following correctness table 2 CComplete and Sufficient SSufficient only N Neither Compound Programs and the Axiom of Replacement The algebraic structure of compound program P permits decomposition into a hierarchy of abstractions The proof of correctness of P is thereby decomposed into a proof of correctness of each such abstraction Compound Programs and the Axiom of Replacement conl d For example to show that compound program F implements function f where F ifp then G else H and G H are themselves programs hypothesize functions 9 h and attempt to prove g G and h H Compound Programs and the Axiom of Replacement conl d If successful use the Axiom of Replacement to reduce the problem to proving f ifp then 9 else h If successful again you will have proved fF Compound Programs and the Axiom of Replacement conl d Thus the Axiom of Replacement allows one to prove the correctness of complex programs in a bottom up incremental fashion In the next lecture we consider correctness conditions for sequencing and decision statements Functional Verification Software Testing and Veri cation Lecture 2 1 Prepared by Stephen M Thebaut PhD University of Florida
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'