# Presentation: 758359

## Disciplined Software Engineering Lecture #13

**Software Engineering Institute**
**Carnegie Mellon University**
**Pittsburgh, PA 15213**
**Sponsored by the U.S. Department of Defense**

## Design Verification, Part 2 

**This is the second lecture on design verification.**
**It covers **
**trace tables**
**symbolic execution**
**case checking**
**mathematical program verification**
**program proofs**

## Trace Tables  

**Trace tables are similar to execution tables, but more general.**
**Trace tables examine general program behavior rather than verifying individual cases.**
**Trace tables use**
**symbolic execution**
**case checking**

## Symbolic Execution - 1

**In symbolic execution**
**the program is represented symbolically**
**program behavior is examined analytically**
**   **
**Symbolic execution can produce quite general verifications.**
**Symbolic execution is not always practical.**

## Symbolic Execution - 2

**In symbolic execution, the approach is to**
**assign algebraic symbols to the program variables  **
**restate the program as one or more equations in these symbols**
**analyze the behavior of these equations**

## Symbolic Execution - 3

**   **
**Some questions to ask are**
**does the program converge on a result?**
**how does the program behave for both normal and abnormal input values?**
**does the program always produce the desired results?**

## Symbolic Execution Example 

**Given the following simple program segment**
**    ****begin**
**       ****V1 = V2**
**       ****V2 = V4**
**       ****V3 = V1**
**       ****V4 = V3**
**    ****end**
**What would be the result for various values of V1, V2, V3, and V4?**

## The Symbolic Trace Table

**The trace table for this example would look like this:**
**Thus the result, for inputs A, B, C, and D is B, D, B, and B.**

**#**

**Instruction**

**V1**

**V2**

**V3**

**V4**

**Initial values**

**A**

**B**

**C**

**D**

**1**

**V1 = V2**

**B**

**2**

**V2 = V4**

**D**

**3**

**V3 = V1**

**B**

**4**

**V4 = V3**

**B**

**Final values**

**B**

**D**

**B**

**B**

## Symbolic Execution Exercise

**Determine the values for which the following program will terminate.**
**Calculate(x: real)**
**   ****if x>0**
**      ****x=sqrt(x)-1**
**   ****else**
**      ****x=-x**
**   ****if x<>0**
**      ****Calculate(x)**
**end.**

## Exercise Result - 1

**The variables can be represented by x1 and x2.**
**The equation for the result of each cycle is**
**   ****if x1>0: x2 = sqrt(x1) -1 **
**   ****if x1 <= 0: x2 = -x1 **

## Exercise Result - 2

**For x1 = 0, the program terminates on the first cycle.**
**For x1 = 1, the program terminates on the first cycle.**
**For x1 = -1, the program terminates on the second cycle.**

## Exercise Result - 3

**Working backwards**
**for x2 to be 1, x1 would have to be 4**
**for x2 to be 4, x1 would have to be 25**
**for x2 to be 25, x1 would have to be 676**
**for x2 to be 676, x1 would have to be 458329**
**and so forth  **
**Thus, the program terminates for input values of + or - 1, 4, 25, 676, 458329, etc.**

## Exercise Result - 4

**For other large positive or negative values of x1, the value of x2 will converge to a non-zero number between -1 and +1.**
**What happens for non-zero values between -1 and +1?**

## Exercise Result - 5

**Pick x1=a, a very small number**
**x2=sqrt(a)-1, a negative number**
**next, x2 is made positive **
**in 2 more cycles, x2 is approximately sqrt(a)/2, or slightly larger than a**
**For small x1, the value of x2 thus gradually grows larger than x1.**
**The value of x2 will thus not reach 0 but will converge on some number less than 1.**

## Exercise Result - 6

**When the value converges, x1 = x2 = x and the result would be given by the equation**
** **
**   ****sqrt(x) - 1 = -x**
**the solution to this equation is**
**   ****x = [3 - sqrt(5)]/2 = 0.381966**
**Thus, the program will end up cycling between the values of + and - 0.381966.**

## Symbolic Execution Advantages

**Symbolic proofs can be general.**
**Symbolic proofs typically involve less work than other methods.**
**Symbolic proofs are less error prone than executing test cases.**

## Symbolic Execution Disadvantages

**Symbolic execution is hard to use except for algorithmic and substitution problems.**
**Symbolic execution proofs are manual and thus error prone.**
**Symbolic execution is difficult to use with complex logic.**

## Case Checking - 1 

**Case checking involves the following steps**
**1.  Examine the program and determine the **
**     ****various categories of program behavior.**
**2.  For these categories, identify the cases to be **
**     ****checked.  **
**3.  Check the cases to ensure that they cover all **
**     ****possible situations.  **

## Case Checking - 2 

**4.  Using trace tables, either alone or with **
**     ****symbolic execution or proof by induction, **
**     ****examine program behavior for each case.**
**5.  Once every case has been verified, program **
**     ****behavior has been verified.**

## Trace Table Example - 1

**The ClearSpaces program requirements**
**clears the leading and trailing spaces from a character string**
**leaves the imbedded spaces in place**
**produces a state value 0 for an empty string**
**produces a state value 1 for a 1 space string**
**produces a state value 2 for a 2 or more space string**
**produces a state value 3 for a string containing non-space characters.**

## Trace Table Example - 2

**ClearSpaces(var Input: string; State: int)**

**Length = length(Input)**

**if Length > 0**

**repeat(until State=3 or Length=0)**

**if Input[Length-1] = ‘ ‘**

**Length = Length - 1**

**if State < 2 State=State+1**

**else State = 3**

**until State=3 or Length=0**

**The portion of ClearSpaces for removing trailing spaces is **

## Trace Table Example - 3

**To define the cases for trailing spaces, establish the following conventions**
**1.  A message string is a string starting and **
**     ****ending with a non-space character.**
**2.  An input string will consist of m message **
**     ****characters and t trailing spaces**
**3.  m is either >0 or 0**
**4.  t is either >0 or 0**

## Trace Table Example - 4

**There are thus a total of 4 cases**
**1.  0-0: m = 0, t = 0**
**2.  0-t:  m = 0, t > 0**
**3.  m-0:  m > 0, t = 0**
**4.  m-t:  m > 0, t > 0**

## Trace Table Example - 5

**The strategy is to verify program behavior with each case, using whatever method is most appropriate.**
**1.  Check the 0-0 case by itself, using an **
**     ****execution table.**
**2.  Check the other cases, using proof by **
**     ****induction. **
**3.  Do each proof with a trace table, using**
**     ****the execution table method described in **
**     ****lecture 12.**

## Verifying Program Correctness

**These methods are based on treating programs as mathematical theorems.**
**They are particularly useful during design and design review.**
**Because program verification often involves sophisticated reasoning, it is important to check your work carefully.**

## Correctness Verification 

**The correctness verification approach is to**
**identify all the program cases.**
**use trace tables to evaluate all the conditions the program must satisfy for every case**
**use proof by induction where appropriate**
**The program is verified if all the conditions are satisfied for every case.**
**While this verification approach works with most design constructs, only loops are described in this lecture.**

## ForLoop Verification - 1 

**The ForLoop is assumed to have the following form**
**ForLoop**
**  ****for n = First to Last**
**    ****begin**
**      ****nPart**
**    ****end**

## ForLoop Verification - 2 

**The for-loop conditions require that the answer to the following question be true**
**Does ForLoop = FirstPart+SecondPart+...+LastPart**

## ForLoop Example - 1

**Verify that the following program produces the factorial of n.**
**factorial(n)**
**  ****begin**
**    ****x=1**
**    ****for i=1 to n**
**      ****x = x*i**
**    ****return = x**
**  ****end**

## ForLoop Example - 2

**First, identify the cases.**
**The cases are for n = 1 and for n > 1.**
**For n = 1**
**      ****ForLoop = 1! = 1**
**      ****FirstPart+SecondPart+...=FirstPart = 1*1=1**
**      **
**The case for n = 1 is thus valid.**

## ForLoop Example - 3

**For n > 1, say 3**
**   ****ForLoop = 3! = 6**
**   ****FirstPart+SecondPart+ThirdPart = 1*1*2*3 = 6**
**   **
**The case for n = 3 is thus true.**

## ForLoop Example - 4

**Next, use proof by induction to verify performance at all higher values of n.**
**Assume that operation is verified for n = k.**
**    ****ForLoop = k! and**
**    ****FirstPart+...LastPart = 1*1*2*3*4*...*k = k!**

## ForLoop Example - 5

**Now, for k+1**
** **
**    ****ForLoop = k!*(k+1) = (k+1)!**
**    ****FirstPart+...LastPart = 1*1*2*3*4*...*k*(k+1)**
**    ****= (k+1)!**
**The program is thus valid for k+1 so, by induction, it is valid for all values of n => 1.**
**You should next check to find any k values on your system where this is not true.**

## WhileLoop Verification - 1 

**The WhileLoop is assumed to have the following form**
**WhileLoop**
**  ****while WhileTest**
**    ****begin**
**      ****LoopPart**
**    ****end**

## WhileLoop Verification - 2

**Question 1.  Is loop termination guaranteed for any argument of WhileTest?**
**  **
**Question 2.  When WhileTest is true does**
** ****WhileLoop = LoopPart followed by WhileLoop?**
**Question 3.  When WhileTest is false does**
** ****WhileLoop = identity?**

## WhileLoop Example - 1

**Use the first part of a program to reduce a floating point number to standard form.**
**Exp is a positive integer **
**Mant is to be made a positive non- zero number with one digit before the decimal point.**
**NormalizeReal(Mant, Exp, NegEx)**
**  ****while Mant >= 10 do**
**    ****Mant = Mant/10**
**    ****if NegEx then Exp=Exp-1**
**    ****else Exp = Exp + 1**

## WhileLoop Example - 2

**Since the value of Exp is not material, there are 3 cases of interest.  **
**Each of these cases is examined for NegEx true and NegEx false.**
**1.  Mant <10**
**2.  Mant = 10**
**3.  Mant > 10**

## WhileLoop Example - 3 

**Question 1.  Is loop termination guaranteed for any argument of WhileTest?**
**  **
**Case 1.  Mant < 10, the while test fails immediately, so the loop terminates.**
**Case 2.  Mant = 10, the while test will fail after one cycle, thus terminating the loop.**
**In both cases, this happens regardless of the value of NegEx.**

## WhileLoop Example - 4 

**Question 1, continued**
**Case 3.  Mant > 10, can be shown by induction**
**Mant = k*10**n, where 1 <= k < 10 **
**when n = 1, the test fails after 1 cycle**
**if the test is true for some value n=m then after m cycles, Mant = k**
**thus for n=m+1, after m cycles, Mant = k*10   and the WhileTest will fail in one more cycle**
**Since the value of NegEx does not affect the result, question 1 is satisfied for all n => 1.**

## A WhileLoop Example - 5

**Question 2.  When WhileTest is true does**
**  ****WhileLoop = LoopPart followed by WhileLoop?**
**Case 1.  Mant < 10, is not pertinent since WhileTest is never true.**

## A WhileLoop Example - 6

**To examine the other cases, check that this  program gives the same result as WhileLoop (the check is described in the next foil).**
**  ****Mant = Mant/10**
**  ****if NegEx then Exp=Exp-1**
**    ****else Exp = Exp + 1**
**  ****while Mant >= 10 do**
**    ****Mant = Mant/10**
**    ****if NegEx then Exp=Exp-1**
**      ****else Exp = Exp + 1**

## A WhileLoop Example - 7

**Question 2 - continued**
**For case 2.  Mant = 10, the value of NegEx is immaterial**
**WhileLoop has one cycle, leaving Mant = 1**
**LoopPart followed by WhileLoop starts with Mant = 10, LoopPart leaves value 1, and WhileLoop leaves the same value 1**
**   **
**Since both give the same result, the answer is true.**

## WhileLoop Example - 8 

**Question 2 -  Continued**
**    **
**Case 3.  Mant > 10, can be shown by induction.**
**Mant = k*10**n, where 1<=k<10 **
**when n = 1, WhileLoop would take one cycle and the WhileLoop following the LoopPart would take none**
**when n > 1 the While Loop following LoopPart    would take one less cycle with the same result **
**Question 2 is thus satisfied for all cases.**

## WhileLoop Example - 9

**Question 3.  When WhileTest is false does    WhileLoop = identity?**
**Case 1.  Mant < 10 is the only case where WhileTest is false.**
**Since, in this case the program is not executed,   the conditions are left undisturbed which is the definition of identity.**
**Question 3 is thus satisfied.**

## RepeatUntil Verification - 1

**RepeatUntil has the following form**
**     ****RepeatUntil**
**       ****begin**
**          ****LoopPart**
**          ****UntilTest**
**       ****end**

## RepeatUntil Verification - 2

**Repeat-until verification is satisfied if the answers to the following 3 questions are true.**
**Question 1.  Is loop termination guaranteed for any argument of UntilTest?**
**Question 2.   When the UntilTest after LoopPart is false, does**
** **
**RepeatUntil = **
**     ****LoopPart followed by RepeatUntil?**

## RepeatUntil Verification - 3

**Question 3.  When UntilTest after LoopPart is true, does**
**      ****RepeatUntil = LoopPart?**
**The repeat-until verification follows the same logical format as WhileLoop verification so no example is given. **

## Comments on Program Verification - 1

**If done correctly, these verification methods are quite general and can guarantee program correctness.**
**The verification methods are tricky and require skill.**
**While you should attempt to use these methods, when in doubt, check with a trace table or an execution table. **

## Comments on Program Verification - 2

**With practice, you can do program verification quite rapidly.**
**The careful examination of all possible cases will quickly reveal most defects.**
**The loop termination test is critical because endless loops are hard to identify with other methods.**

## Lecture #13 Assignment

**Start work on the final report.**
**Update the process used to develop the mid-term report and use it to develop the final report.**
**Turn in the updated process, the plan for the work, the actual data for the work, and the final report.**
**Consult the report specifications in Appendix D.**

## Messages to Remember from Lecture 13 

**1.  There are many powerful verification **
**     ****techniques.**
**2.  Experiment with these techniques, find the **
**     ****ones that are most effective for you, and use **
**     ****them.**
**3.  The time you spend verifying designs will be **
**     ****repaid many times by the testing time you **
**     ****save.**