# Lösungsvorschlag Formal Methods and Functional Programming FS07

## Assignment 1 (Set Theory)

### 1.1)

${\displaystyle P(B)\times B=\{\{\}\,B\}\times \{0\}=\{\{\}\mapsto 0,\{0\}\mapsto 0\}}$
${\displaystyle (P(B)\times B)(\emptyset )=\{0\}}$
${\displaystyle S[B]\cap T=\{4\}}$

### 1.2)

${\displaystyle (B\cup T)\times B=\{0,2,4,8\}\times \{0\}}$ ${\displaystyle F=\{0\mapsto 0\}}$

### 1.3)

${\displaystyle \forall x\cdot (\exists y\cdot y\in A\wedge y\mapsto x\in p\wedge x\in B)\Rightarrow (\exists z\cdot z\in A\wedge z\in A\wedge x\in B)}$

## Assignment 2 (Model of an Access Control System)

### 2.1)

inv0_2: ${\displaystyle loc\in PERSON\nrightarrow ROOM}$

### 2.2)

${\displaystyle p\notin dom(loc)}$

### 2.3)

enter/inv0_2/INV:

${\displaystyle H\in ROOM}$
${\displaystyle loc\in PERSON\leftrightarrow ROOM}$
${\displaystyle loc\in PERSON\nrightarrow ROOM}$
${\displaystyle p\notin dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle loc\cup \{p\mapsto H\}\in PERSON\nrightarrow ROOM}$


### 2.4)

 enter/inv0_2/INV 

${\displaystyle H\in ROOM}$
${\displaystyle loc\in PERSON\leftrightarrow ROOM}$
${\displaystyle loc\in PERSON\nrightarrow ROOM}$
${\displaystyle p\notin dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle loc\cup \{p\mapsto H\}\in PERSON\nrightarrow ROOM}$


FUN

 FUN Branch 1: ${\displaystyle H\in ROOM}$ ${\displaystyle loc\in PERSON\leftrightarrow ROOM}$ ${\displaystyle loc\in PERSON\nrightarrow ROOM}$ ${\displaystyle p\notin dom(loc)}$ ${\displaystyle \vdash }$ ${\displaystyle loc\in PERSON\nrightarrow ROOM}$  MON ${\displaystyle loc\in PERSON\nrightarrow ROOM}$ ${\displaystyle \vdash }$ ${\displaystyle loc\in PERSON\nrightarrow ROOM}$  HYP FUN Branch 2: ${\displaystyle H\in ROOM}$ ${\displaystyle loc\in PERSON\leftrightarrow ROOM}$ ${\displaystyle loc\in PERSON\nrightarrow ROOM}$ ${\displaystyle p\notin dom(loc)}$ ${\displaystyle \vdash }$ ${\displaystyle p\notin dom(loc)}$  MON ${\displaystyle p\notin dom(loc)}$ ${\displaystyle \vdash }$ ${\displaystyle p\notin dom(loc)}$  HYP

### 2.5)

Aufgabe 2.5 entspricht Exercise 14.5. Die Lösung dazu ist jetzt online.

DLF

${\displaystyle \exists p\cdot p\in PERSON}$

${\displaystyle \vdash }$

${\displaystyle (\exists p\cdot (p\notin dom(loc))\vee }$
${\displaystyle [(p\in dom(loc)\wedge loc(p)=H)\vee }$
${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)])}$


XST_L, XST_R, CASE

CASE Branch 1:

MON

${\displaystyle p\notin dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle (p\notin dom(loc))\vee }$
${\displaystyle [(p\in dom(loc)\wedge loc(p)=H)\vee }$
${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)]}$


OR_R1

${\displaystyle p\notin dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle p\notin dom(loc)}$


HYP

CASE Branch 2:

MON, Rewriting ${\displaystyle \notin }$

${\displaystyle p\in dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle (p\notin dom(loc))\vee }$
${\displaystyle [(p\in dom(loc)\wedge loc(p)=H)\vee }$
${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)]}$


OR_R2

${\displaystyle p\in dom(loc)}$

${\displaystyle \vdash }$

${\displaystyle (p\in dom(loc)\wedge loc(p)=H)\vee }$
${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)}$


CASE

 CASE Branch 1: ${\displaystyle p\in dom(loc)}$ ${\displaystyle loc(p)=H}$ ${\displaystyle \vdash }$ ${\displaystyle (p\in dom(loc)\wedge loc(p)=H)\vee }$ ${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)}$  AND_L, OR_R1 ${\displaystyle p\in dom(loc)\wedge loc(p)=H}$ ${\displaystyle \vdash }$ ${\displaystyle p\in dom(loc)\wedge loc(p)=H}$  HYP CASE Branch 2: ${\displaystyle p\in dom(loc)}$ ${\displaystyle \neg (loc(p)=H)}$ ${\displaystyle \vdash }$ ${\displaystyle (p\in dom(loc)\wedge loc(p)=H)\vee }$ ${\displaystyle (\exists r\cdot p\in dom(loc)\wedge loc(p)\neq r)}$  Rewriting ${\displaystyle \neg }$, AND_L, OR_R2 ${\displaystyle p\in dom(loc)\wedge loc(p)\neq H}$ ${\displaystyle \vdash }$ ${\displaystyle \exists r\cdot p\in dom(loc)\wedge loc(p)\neq r}$  XST_R with r=H, HYP

## Assignment 3 (Refinement of Access Control System)

Bin mir nicht ganz sicher: Vorsicht!

### 3.1)

${\displaystyle id(ROOM)\subseteq door;door^{-1}}$

Ich glaube eine einfachere Lösung wäre: ${\displaystyle door=door^{-1}}$ Ist symmetrisch. (Slide 168 in math)

### 3.2)

${\displaystyle ran(\{H\}\triangleleft door)=ROOM\setminus \{H\}}$

### 3.3)

${\displaystyle dom(auth\triangleright \{H\})=PERSON}$

### 3.4)

 Diese Aufgabe wurde noch von niemandem gelöst und wartet noch immer auf einen Musterlöser. Hast du dieses Fach bereits besucht? Hilf mit, die Qualität dieser Seite zu verbessern, indem du eine plausible Lösung für diese Frage notierst!

## Assignment 4 (Euclid's Algorithm)

m>n

m<n

n:= n-m

### 4.5)

Genau gleich wie exercise 13, Third Refinement. M_IF, M_WHILE, M_INIT