### Create a StudySoup account

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

Already have a StudySoup account? Login here

# SOFTWAREFOUNDATIONS CIS500

Penn

GPA 3.73

### View Full Document

## 9

## 0

## Popular in Course

## Popular in Computer Information Technology

This 11 page Class Notes was uploaded by Kathleen Cartwright on Monday September 28, 2015. The Class Notes belongs to CIS500 at University of Pennsylvania taught by B.Pierce in Fall. Since its upload, it has received 9 views. For similar materials see /class/215372/cis500-university-of-pennsylvania in Computer Information Technology at University of Pennsylvania.

## Reviews for SOFTWAREFOUNDATIONS

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

C18 500 i Software Foundations Midterm I Review questions with answers October 10 2007 Work each of the review problems yourself before looking at the answers given here If your answer differs from ours7 make sure you understand why P E0 Functional Programming Consider the following Fixpo int de nition in Coql Fixpoint fold XSet YSet f XgtYgtY 11ist X bY struct 1 match 1 with Inilgtb Ihtgtfhfoldftb end What is the type of fold lie7 What does Check fold print Answer fold forall X Y Set X gt Y gt Y gt list X gt Y gt Y What does Check fold plus print Answer fold nat nat plus list nat gt nat gt nat What does Eval simpl in fold plus onetwothreefour one print Answer eleven nat Recall that the map function takes a function f of type XgtY and a list 1 With elements of X and returns a list With elements of type Y containing the result of applying f to each element of 1 Which of the following Fixpoint de nitions correctly implements the map function Circle the correct answer a Fixpoint m1 XSet YSet fXgtY 11ist X struct 1 match 1 with I nil gt nil Y I h t gt h list Y 2 m1 X Y f t end b Fixpoint m2 XSet YSet fXgtY 11ist X struct 1 list Y match 1 with I nil gt f nil Y I h t gt f h m2 X Y f t end c Fixpoint m3 XSet YSet fXgtY 11ist X struct 1 list Y match 1 with I nil gt nil Y I h t gt f h m3 X Y f t end d Fixpoint m4 XSet YSet fXgtY 11ist X struct 1 list Y matchlwithInilgtni1YIhtgtfhfm4Xth end e Fixpoint m5 XSet YSet fXgtY 11ist X struct 1 list Y matchlwithInilgtnilYIhtgtfhftend f None of the above Answer 0 5 The every function takes a predicate p a oneargument function returning a yesno and a list 1 it returns yes if p returns yes on every element of 1 and no otherwise Lemma checkfi1ter1 every nat even twofourzero yes Proof simp1 reflexivity Qed Lemma checkfi1ter2 every nat even twoonefourzero no Proof simp1 reflexivity Qed What is the type of every Answer forall X Set X gt yesno gt list X gt yesno 6 Complete the following de nition of every as a recursive function Fixpoint every XSet pXgtyesno 11ist X struct 1 yesno match 1 with I ni1 gt I h t gt bothyes end Answer Fixpoint every XSet pXgtyesno 11ist X struct 1 yesno match 1 with I ni1 gt yes I h t gt bothyes p h every p t end 7 Complete the following de nition of every by supplying appropriate arguments to fold Definition every XSet pXgtyesno 11ist X yesno fold fun x acc gt bothyes Answer Definition every XSet pXgtyesno 11ist X yesno fold fun x acc gt bothyes p x ace 1 yes Coq Basics Brie y explain the difference between the tactics apply and rewritel Are there situations Where either 9 one can be applied Answer The rewrite tactic is used to apply a known equality to either the goal or a hypothesis in the context replacing all occurrences of one side by the other The apply tactic uses a known implication a hypothesis from the context a previously proved lemma or a constructor to modify the proof state either backward the goal matches the conclusion of the implication in which case a subgoal is generated for each premise of the implication or forward some hypothesis matches the premise of the implication in which case this hypothesis is replaced by the conclusion of the implication If the fact is itself an equality e an implication with no premises then either tactic can be use Brie y explain the difference between the tactics destruct and induction Answer Both are used to perform case analysis on an element of an inductively de ned type induction also generates an induction hypothesis while destruct does not 50 10 The following proof attempt is not going to succeed Brie y explain Why and how it can be xed Lemma doub1einjective forall m n double m double n gt m n Proof intros m n induction m Case quot0quot simpl intros eq destruct n Case quot0quot reflexivity Case quotSquot inversion eq Case quotSquot intros eq destruct n Case quot0quot inversion eq Case quotSquot assert m n as H Case quotProof of assertionquot Answer Because the induction hypothesis is insu iciently general 7 it gives us a fact involving one particular n but to nish the last step of the proof we need to know something about a di erent n To x it either use generalize dependent n before induction or else just omit intros m n Inductively De ned Sets 11 Suppose we give Coq the following declarations Inductive mumble Set I a mumble I b mumble gt nat gt mumble I c mumble Inductive grumble XSet Set I d mumble gt grumble X I e X gt grumble X Which of the following are welltyped members of the set grumble a d b a five Answer No b d mumble b a five Answer Yes c d yesno b a five Answer Yes d e yesno yes Answer Yes e e mumble b c zero Answer Yes f e yesno b c zero Answer No g c Answer No H E0 Consider the following inductive de nition Inductive baz Set I x baz gt baz I y baz gt yesno gt baz How many elements does the set baz have Answer None 13 Consider the following inductive de nition Inductive tree Set I leaf tree I node tree gt tree gt tree Describe7 in English7 the elements of the set treei Answer Unlabeled binary trees 14 What induction principle Will Coq generate for tree Answer treeind forall P tree gt Prop leaf gt forall t tree gt forall t0 tree P to gt P node 1 110 gt forall t tree P 1 Alternate answer the one above is What Coq actually generates7 but it is logically equivalent to this arguably more natural variant treeind forall P tree gt Prop P leaf gt forall t1 t2 tree P 131 gt P 132 gt P node 131 112 gt forall t tree P t 15 Here is an induction principle for an inductively de ned set 5 mysetind forall P myset gt Pro forall y yesno P conl y gt forall n nat m myset P m gt P con2 n m gt forall m myset P In What is the de nition of myset Answer Inductive myset Set I conl yesno gt myset I con2 nat gt myset gt myset 16 Consider the following inductive de nition nat gt Set Inductive stree I leaf stree one forall m n stree m gt stree n gt stree plus m n I node Describe7 in English7 the elements of the set stree seveni Answer Unlabeled binary trees with exactly seven leaves In general for each n the set stree it contains binary trees with n total leaves Inductively De ned Propositions 17 Consider the following inductively de ned family of propositions Inductive p tree gt nat gt Prop 2 I c1 p leaf one I c2 forall t1 t2 n1 n2 p t1 n1 gt p t2 n2 gt p node t1 t2 plus n1 n2 Describe7 in English7 the conditions under Which the proposition p t n is provablel Answer This proposition is provable when t is an unlabeled binary tree with exactly n leaves That is p is a relation between trees and numbers that relates each tree to its number of leaves 18 Consider the following inductively de ned family of propositions Inductive bar nat gt Prop I d bar six I e forall 11 bar times n n I f bar three gt bar five For Which n is the proposition bar n provable Answer bar n is provable when n is either six or a perfect square zero one four nine etc Programming With Propositions 19 The concept of composition of relations can be de ned as follows Suppose Q and R are both relations on a set X The composition of Q and R is the relation C such that7 for all x and z in X7 sz lt gt HlexyARyzl Write an Inductive de nition in Coq that expresses this concept Answer Inductive composition X Set Q R relation X X gt X gt Prop comp forall x 2 exists y Q x y R y z gt composition X Q R x z 20 Give the de nition of logical conjunction and as an inductive proposition in Coql Answer Inductive and A B Prop Prop 2 conj A gt B gt and A B Operational Semantics 21 Recall the de nition of the set tm7 the predidate value7 and the relation eval from the lecture notes Inductive tm Set I tmconst nat gt tm I tmplus tm gt tm gt tm Inductive value tm gt Prop 2 vconst forall n value tmconst n Inductive eval tm gt tm gt Prop I EPlusConstConst forall n1 n2 eval tmplus tmconst n1 tmconst n2 tmconst plus n1 n2 I EPlus1 forall t1 t1 t2 eval t1 t1 gt eval tmplus t1 t2 tmplus t1 t2 I EPlus2 forall v1 t2 t2 value v1 gt eval t2 t2 gt eval tmplus v1 t2 tmplus v1 t2 Which of the following propositions are provable a eval tmplus tmconst one tmconst two tmconst plus one two Answer Yes b eval tmplus tmplus tmconst one tmconst two tmconst three tmconst plus plus one two three Answer No c eval tmplus tmplus tmconst one tmconst two tmplus tmconst three tmconst four tmplus tmplus tmconst one tmconst two tmconst plus three four Answer No Recall the determinism and progress theorems for the eval relation Theorem eva1deterministic partia1function eval Theorem eva1progress forall t value 1 exists t eval t t a Suppose we add a new constructor to the evaluation relation as follows N N I EFunny1 eval tmconst zero tmconst zero ii Does eva1deterministic continue to hold Answer No iii Does eva1progress continue to hold Answer Yes b Suppose we remove the constructor vconst from the de nition of value ii Does eva1deterministic continue to hold Answer Yes iii Does eva1progress continue to hold Answer No c Is there any way we can cause eva1progress to fail by adding new constructors to the de nition of eval Answer No

### 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 used the money I made selling my notes & study guides to pay for spring break in Olympia, Washington...which was Sweet!"

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