### Create a StudySoup account

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

Already have a StudySoup account? Login here

# Programming Languag Foundatn I EECS 762

KU

GPA 3.74

### View Full Document

## 32

## 0

## Popular in Course

## Popular in Elect Engr & Computer Science

This 3 page Class Notes was uploaded by Melissa Metz on Monday September 7, 2015. The Class Notes belongs to EECS 762 at Kansas taught by Perry Alexander in Fall. Since its upload, it has received 32 views. For similar materials see /class/184020/eecs-762-kansas in Elect Engr & Computer Science at Kansas.

## Popular in Elect Engr & Computer Science

## Reviews for Programming Languag Foundatn I

### 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/07/15

Semantic Equivalence Proof Examples Dr Perry Alexander EECS 662 Programming Language Foundation The University of Kansas November 3 2008 The purpose of this document is to provide examples of cases from a structural induction proof that the denotational semantics and operational semantics de ned for IMP by Winskel are equivalent We will speci cally look at showing Cc000 ltc0gtgt 0 1 for cases where c is a command de ned in IMP The rst case to examine is sequencing of commands co cl as a prototypical example of verifying command seman tics In this case the proof goal abstractly de ned as equation 1 has the form Ccocl0 00 lt co 010 gtgt 0 2 From the de nition of C we know the left side of equation 2 can be rewritten as 00 l 30 E E Cco0 0 Ccl0 0 3 Resulting in the proof obligation 00 l 30 E E Cco0 0 Ccl0 0 00 lt cocl0 gtgt 0 4 By the de nition of set comprehension equation 1 1 can be rewritten as 30 E E Cco0 0 Ccl0 0 ltgtlt co 010 gtgt 0 5 From the overall structural induction proof we have the induction hypotheses CC00 0 ltgt lt C070 gtgt 0 6 CC10 0 ltgt lt Cl7 0 gtgt 0 7 To establish 12 we have two cases Case 1 30 Cco0 0 AC010 0 lt C0 C170 gtgt 0 To prove the implication we assume the antecedent and prove the consequent Assuming CC00 0 and CC10 0 it follows from the induction hypothesis that lt 007 0 gtgt 0 and lt C1 0 gtgt 0 Recall from the operational semantics de nition of IMP the rule for deriving C0 C1 ltcoagtgt a ltclagtgt 0 8 equal a lt co 010 gtgt 0 The induction hypothesis gives the precondition of the rule thus it follows that lt C0 C1 0 gtgt a which is the goal of Case 1 Case 2 Ha Ccoa a Ccla 0 lt co 010 gtgt 0 Note that sequence is the only rule in the operational semantics of IMP that derives lt co 510 gtgt 0 Thus assuming that lt co cl 0 gtgt a is derivable the rule sequence must be the last rule applied in the derivation Thus the preconditions of sequence must be true in the derivation It then follows directly from the induction hypothesis that Ccoa a Ccla 0 which is the goal of this case Having proved both cases from equation 12 we have proved the conjecture QED The second case to examine is the while loop whiledeC as a more aggressive example of verifying command seman tics In this case the proof goal abstractly de ned as equation 1 has the form Cwaaallt 100 gtgta 9 where w while b do 5 From the de nition of C we know the left side of equation 9 can be rewritten as Cwa fizFs0 U Mu lt10 new Recall the de nition of go is really C wa Here the proof obligation is a bit different as we re looking a xed point The xed point is wellde ned and indexed on w thus a proof by induction over the natural numbers is in order Recall the following de nitions ROGD R 108 070 l Bllbl l true A aysigma 6 Cllcll A WW 6 R Thus we have a base case and an inductive case for an induction over n Our proof goal is Vn E w 070 E lt 010 gtgt 0 11 The base case is trivial as the left side reduces to 07 sigma E which is false Thus by contradiction the right side is true For the inductive case we Will assume that 070 E lt a w gtgt 0 and show that W e Rn1ltgt lt a w gta a

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