### Create a StudySoup account

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

Already have a StudySoup account? Login here

# SOFTWARE ENGINEERING CEN 5035

UF

GPA 3.57

### View Full Document

## 19

## 0

## Popular in Course

## Popular in Computer Engineering

This 41 page Class Notes was uploaded by Paxton Okuneva on Saturday September 19, 2015. The Class Notes belongs to CEN 5035 at University of Florida taught by Stephen Thebaut in Fall. Since its upload, it has received 19 views. For similar materials see /class/207039/cen-5035-university-of-florida in Computer Engineering at University of Florida.

## Reviews for SOFTWARE ENGINEERING

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

Proofs of Correctness An Introduction to Axiomo c Verification CEN 5035 Software Engineering Prepared by Stephen M Thebouf PhD Universiry ofFon39do Outline Introduction Weak correctness predicate Assignment statements Sequencing Selection statements Iteration Introduction What is AXiomatic Veri cation A formal method of reasoning about the functional correctness of a structured sequential program by tracing its state changes from an initial ie pre condition to a final ie post condition according to a set of self evident rules ie axioms Introduction conl d What is its primary goal To provide a means for proving or disproving the functional correctness of a sequential program with respect to its formal speci cation Introduction coni d What are the bene ts ofstudying axiomatic verification Understanding its limitations Deeper insights into programming and program structures Criteria for judging both programs and programming languages The ability to formally verify small or parts of large sequential programs Introduction coni d Bottom line even if you never attempt to prove a program correct outside this course the study of formal verification should change the way you write and read programs Weak Correctness Predicate To prove that program S is weakly correct with respect to pre condition P and post condition Q it is suf cient to show P S Q Interpretation of P S Q the input initial state satisfies pre condition P and E program S executes and terminates then the output final state will satisfy post condition Q Weak Correctness Predicate conl d Thus P S Q is true unless Q could be false if S terminates given that P held before S executes What are the truth values of the following assertions ll Xl i gtltl ygt0 Weak Correctness Predicate conl d Thus P S Q is true unless Q could be false if S terminates given that P held before S executes What are the truth values of the following assertions 2 xgt0 x xi xgt0 Weak Correctness Predicate conl d Thus P S Q is true unless Q could be false if S terminates given that P held before S executes What are the truth values of the following assertions 3 i2 llt 5 klt0 Weak Correctness Predicate conl d Thus P S Q is true unless Q could be false if S terminates given that P held before S executes What are the truth values of the following assertions 4 True while x ltgt 5 do x xi x5 Hint When will S terminate Weak Correctness Predicate conl d We now consider techniques for proving that such assertions hold for structured programs comprised of assignment statements if then else statements and while loops Why these particular constructs Reasoning about Assignment Statements For each of the following pre conditions P and assignment statements S identify a strong post condition Q such that P S Q would hold A strong post condition captures all alter execution state information of interest We won t bother with propositions such as XX the nal value of X is the same as the initial value of X for the time being rd Reasoning about Assignment Statements cont d Qt J6 K 3 J6 J J2 AltB Min A gtltlt0 Y gtlt NA l Reasoning about Assignment Statements cont d For each of the following post conditions Q and assignment statements S identify a weak pre condition P such that P S Q would hold A weak pre condition reflects only what needs to be true before and Reasoning about Assignment Statements cont d When does P S Q gt K S W We just determined that J7 1 4 J7 14 holds We can deduce from this that J7 14 J7 also holds since J7 14 is stronger than J7 That is because J7 14 2 J7 When does P S Q K S W conl d Similarly if we know that J7 1 4 J7 A 14 holds it follows that J7 A Ki 7 1 4 J7 A 14 also holds since J7 is weaker than J7 Ki7 That is because J7 A Ki 7 gt J7 When does P S Q K S W conl d Thus we can replace pre conditions with ones that are stronger and post conditions with ones that are weaker Note that ifA 2 B we say that A is stronger than B or equivalently that B is weaker than A Practice quiz question In general which would be the better marketing strategy for increasing your software salesadvertising the software as having a strong pre condition and a weak post condition or vice versa Give a concrete example which illustrates your answer Reasoning about Sequencing In general if you know PS1 R and you know R S2 Q then you know P S1 S2 Q So to prove P S1 S2 Q nd R Example 1 Prove the assertion A5 B A2 c BA D AC A5 A D3 ml Reasoning about tthenelse Statements Consider the assertion P if b then S1 else S2 Q P Q What are the necessary conditions for this assertion to hold Necessary Conditions f1henelse Reasoning about tthen Statements Consider the assertion P if b then S Q What are the necessary conditions for this assertion to hold Necessary Conditions Ithen Example 2 Prove the assertion 23 ifAgtB then 2 A ZMoxAB Proof Rules Before proceeding to while loops let s capture our previous reasoning about sequencing selection statements and state condition replacement in appropriate rules ofinference R01 ROI for Sequencing PSl R R 52 Q P Si S2 Q Proof Rules coni d ROI for ifthenese statement P b s Q P bs2 Q P if b then S1 else S2 Q ROI for if then statement PAbSQ PA b Q P if b then S Q Proof Rules coni d ROI for State Condition Replacement K P PS Q ij KS W Reasoning about Iteration Consider the assertion P while b do S Q What are the necessary conditions for this assertion to hold Consider a Loop Invariant I P Suppose I holds initially I b and implies Q when and if the loop finally Q terminates is preserved by S then the assertion would hold Sufficient Conditions whiledo Thus a ROI for the Whiedo statement is P21 IAbSI IA b Q P while b do S Q where the three antecedents are sometimes given the names initialization preservation and finalization respectively Example 3 Use the invariant I ZgtltJ to prove True Initialization P 1 Z gtlt Preservation I b S I J 3 i I While JltgtY do FInaIIzatIon IA ab 2 Q J Ji endiwhile ZgtltY Example 3 Use the invariant I ZgtltJ to prove True Initialization P 1 Z X What is P J 3 i P while JltgtY do ZXAJ 1 z zgtlt Does Zgtlt Ji 2 ZgtltJ J Ji Yep endiwhile ZgtltY Example 3 Use the invariant I ZgtltJ to prove True Initialization P 14 Z X b Preservation I b S I 1 l 2 while JltgtY do Z gtltJ A Y z zgtlt Z 39 zgtlt J JH 5 ZgtltJiJ Y endiwhile J 3 JH Zgtlt Ji i Ji Y Z39XY 2 ZgtltJ Example 3 Use the invariant I ZgtltJ to prove True Initialization P 14 Z 3 X Preservation I b S I I J 3 i I While JltgtY do FInaIIzatIon IA ab 2 Q 2 zgtlt Does ZgtltJ JY 2 ZgtltY J JIi Yep endiwhlle ZgtltY Example 3 Use the invariant I ZgtltJ to prove True Initialization P 14 Z gtlt Preservation I b S I I J 3 i I While JltgtY do FInaIIzatIon IA ab 2 Q I J Ji endiwhile ZgtltY Some Limitations of Formal Verification Difficulties can arise when dealing with parameters pointers synthesis of invariants decidability of veri cation conditions concurrency Some Limitations of Formal Verification cont d In addition a formal speci cation may be expensive to produce may be incorrect andor incomplete normally re ects functional requirements only Will the proof process be manual or automatic Who will prove the proof That s all folks but If you like formal verification Take CEN 6070 Software Testing amp Veri cation and learn about deriving invariants proving termination using the Method of Well Founded Sets Predicate transforms weakest pre conditions function theoretic veri cation prove the correctness of loops without invariants and MUCH more ad

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

#### "I signed up to be an Elite Notetaker with 2 of my sorority sisters this semester. We just posted our notes weekly and were each making over $600 per month. I LOVE StudySoup!"

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

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