Formal Specification in Discrete Mathemateics
Assume a type BOTTLE and an enumerated type COLOUR :2: Green 1 Red and a function colour: BOTTLE -> COLOU R
1. Write a schema WallState with state variable bottlesOnWall :PBOTTLE representing a wall with bottles on it.
2. Write out A WallState and E. WallStateand explain in English what the difference is between these.
3. l throw a stone at the bottles and miss. No bottles fall. Write a schema Jamie Cant Throw ToSaveHisLife expressing this.
4. Somebody else throws a stone at the bottles and knocks a green bottle off the wall. Write a schema GreenBottleKnocked to express this, using input variable thisBottle? Note that your schema should checkjust that thisBottle‘? : BOTTLE is green and on the wall.
5. Write a schema to output the number of green and red bottles on the wall on variables greenBottlesl, redBottles! :N
6. Write a schema Earthquake such that all bottles fall off the wall.
7. HarderA green bottle accidentally falls. Write a schema GreenBottleFalls to express this. Note that there should be no input variable telling us which bottle should fall; some bottle fails by accident and the schema does not specify or control which one.
8. Write a schema McCarthy which removes all the red bottles, leaving the green bottles on the wall for later.
9. Express in logic that everybody has exactly two parents.
10. Write an expression for the siblings ofp (children of both parents ofp, other than p). Assume sets male : PPERSON and female : PPERSON
11. Express in formal logic the assertion that every person is precisely one of male or female.
12. Translate the assertion “I am your father” into logic, for constants Luke,Vader 6 male (see Luke, l am your father; get your answer the right way round, please). (Hint) If your answer begins with “Luke, Vader : PERSON o ” then it’s wrong: Luke and Vader are constants declared in the question, so must be left free (unquantified) in the answer.
13. Write an expression for the uncles of p (brothers of the father of p).
14. Assuming TC(parentOf) (transitive closure) without comment, assert that everybody is descended from p, who is male, and q who is female (see Adam and Eve).
15. (Harder) Assert that there exists a p such that for every q, evehtually every descendent of q is also descended from p (hint: you may assume n -fold composition of relations, such as parentOf” , without comment). Two such p actually exist: see Mitochondrial Eve and Y-chromosomal Adam.
16. (Harder) Write an expression for the step-siblings ofp (children ofa parent ofp who share precisely one parent with p).
17. (Unmarked) Assert that the population bottlenecks through S ; for a fictional account see Children of Men, or for the scientific version see POpulation Bottlenecks.
18. (Unmarked) Express in logic the assertion that q is both the sister and the daughter of p (see Chinatown).