### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# SOFTWARE TESTVERIFI CEN 6070

UF

GPA 3.57

### View Full Document

## 9

## 0

## 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

### 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

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### 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'

## Why people love StudySoup

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "Selling my MCAT study guides and notes has been a great source of side revenue while I'm in school. Some months I'm making over $500! Plus, it makes me happy knowing that I'm helping future med students with their MCAT."

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.