Lösungsvorschlag Formal Methods Endterm 2005

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1 (Logic and Set Theory)

Question 1

(hm, bin nicht sicher ob das mit "Practival Theory" gemeint ist)

1.

2.

[x -> y <-> (y ¬x)]

3.

[De'Morgan]

4.

[Distributivgesetz]

5.

[Distributivgesetz]

6.

[x ¬x <-> true und x true <-> x]

7.

[Assoziativgesetz]

8.

[x ¬x <-> true]

9.

[true ture <-> true]

10.


Bemerkung: ich denke dass mit Practical-Theory die Inference-Rules gemeint sind, hab glaub mal etwas dazu in dem Kapitel "Mathematical Language" gelesen, Beweis ist dann ziemlich einfach =) Hoffe hab nicht ein Schwachsinn geschriben =) Fabiom

Jop, hab ich auch so gemacht, also mit folgenden Regeln nacheinander angewendet: IMP_R, IMP_R, NEG', NEG, IMP_L, MON, HYP --Dhruv 19:05, 2. Jul 2007 (CEST)

Wieso schreibt ihr dann nicht gleich die richtige Lösung hin? (Ja ok, Dhruv's ist nett, aber ich komm dennoch grad nicht drauf wie's geht)

Mein (2.) Versuch (was muss ich für das '?' schreiben?):

Nix =) --Fabiom 23:39, 2. Jul 2007 (CEST)

whee dann kann ich das jetzt auch :)


- - [IMP_R] - -

- - [IMP_R] - -

- - [NEG'] - -

- - [NEG] - -

- - [IMP_L] - -

- - [MON] - -

- - [HYP] - -

Anmerkung: Nach mir könnte man das [MON] weglassen, aber so ist man auf der sicheren Seite --Ldevil 23:33, 2. Jul 2007 (CEST)

Question 2

Habe eine andere Lösung bekommen (stimmt, hatte einen Fehler - thx):

Question 3

Ich verstehe nicht was man mit den Zusatzbedingungen nach where ... machen soll, für den 1. Teil bekomme ich:

zum 'where' : Meiner Meinung nach dient es nur dazu, die Formel zu 'erklären' aber wird zum Lösen nicht gebraucht (vgl. Aufgabe 5.1 und 5.2 in Serie 11)

Assignment 2 (Model Development)

Question 4

ok neuer versuch:


Ich bin der Meinung das ist zu wenig genau ich habe:

Meine Version war etwas umständlich geschrieben das da sollte das Gleiche bedeuten:

inv0_1:

Question 5

stock := { b1 -> 0, b2 -> 0, b3 -> 0, b4 -> 0 }

Alternative:

Question 6

Question 7


  

  

Ich würde die elegantere Methode wählen:


  

  

(oder ist da was falsch dran?) -- Gregr 20:58, 2. Jul 2007 (CEST)

stimmt schon -- Ldevil 21:52, 2. Jul 2007 (CEST)

Question 8

(edit: obs so geht...)

deliver
 any b where
  stock[{b}] /= {0}
 then
  stock := stock <+ {b -> stock[{b}]} ; {x + 1 -> x | x }
 end

edit: Hab mir gedacht, ich mach ne kompsition vom alten b -> stock[{b}] über {1->0, 2->1, ...} und dann mit der neue Relation für b die alte im stock überschreiben. Nur wie ich die Relation {1->0, 2->1, ...} aufschreiben muss weiss ich nicht.

edit2*: ok hab grad gemerkt, dass ich da was verwechselt hab, ja sollte mit 'stock(b) - 1' schon einfach gehen :D

wieso so kompliziert? mit stock(b) kannste ja direkt den wert "holen":

deliver
 any b where
  b  A
 then
  stock := stock <+ {b -> stock(b) - 1}
 end


Hier habe ich mich gefragt, ob es moeglich waere, einfach stock(b) = stock(b)-1 statt stock <+ {b -> stock(b) - 1} zu schreiben. Evtl. akzeptieren sie das.

-> ich würde das nicht riskieren..in diesem fach spielt type safety eine grosse rolle und stock(b) gibt einen integer-wert zurück..du kannst ja auch nicht schreiben 5 := 5-1

Question 9

Proof Obligation deliver/inv0_1/INV:

Properties:
 
Invariants:
 
Guards:
 

 

edit: so nun ist das geänderte 'stock' mit stock(b) drin, was doch etwas einfacher ist.

Informal Proof:

'deliver' ändert nur eine Relation und zwar die von 'b' aus. Dabei wird 'b -> x' mit 'b -> x-1' überschrieben, wobei {x} = stock[{b}] ist, also die Lagermenege von 'b'. max > x > 0, da der Wertebereich von stock in 0..max liegt und zusätzlich gilt, dass stock[{b}] /= {0} (also x /= 0). Die neu hinzugefügte Relation 'b -> x-1' ändert den Wertebereich von stock nicht, da x-1 in 0..(max-1) (und somit auch in 0..max) liegt.

(kA ob das als 'informal' gelten würde)

Question 10

Wir sollen zeigen, dass nach jedem Event immer mind. 1 Guard erfüllt ist:

Proof Obligation:

Properties:
 
Invariants:
 

Guards:
 

Informal proof:

Fallunterscheidung:

Da wir wissen, dass max eine natürliche Zahl ist und dass alle 'beverages' eine Lagermenge zwischen 0 und max haben, ist dies nur der Fall, wenn alle 'beverages' komplett aufgefüllt sind (also ihre Lagermenge 'max' ist), dann gilt aber sicher für ein b womit auch einer der beiden Guards (der von deliver) erfüllt ist.

In diesem Fall ist der Guard von refill erfüllt.

Es gibt keine weiteren Fälle,


-> imho vergisst du den fall, dass max == 0, denn dann ist keiner der beiden guards true. deshalb (vgl. hint) braucht es eine weitere property:

prp0_2: max > 0

Question 11

oder wenn man card() brauchen darf:

Question 12

oder (vgl. Question 6)

Question 13

Event select:

select
 any b where
  stock[{b}] /= {0}
 then
  selected := {b}
 end

Refines skip because:

We add a new event in the first refinement therefore we have to proof that it refines an event of the previous model. Because we didn't introduce it in the previous model, we state that it refines a dummy event skip that is non-guarded and does nothing in the abstract model. The Before-After Predicates of skip are:

stock'=stock
selected'=selected

Kommentar: Da kann etwas nicht stimmen! Das BAP sagt: selected'=selected, aber dabei wird doch der Variable selected ein neuer Wert zugewiesen im Event. Ausserdem: Ich finde da gehört noch der Guard "selected={}" hinein, was aussagt, dass man nicht wählen kann wenn schon gewählt wurde, zumindest nicht bis das Getränk ausgegeben ist. Aber das ist vermutlich Ansichtssache... PeeDee 14:30, 2. Jul 2007 (CEST)

Kommentar2: Ich würd sagen, dass du den Automaten dann ziemlich hassen würdest, wenn man die Wahl nicht mehr ändern kann. kommt aber nicht drauf an, da es nicht in der Aufgabe steht und man soll ja kaum selber Bedingungen hinzudichten. Ldevil 14:35, 2. Jul 2007 (CEST)

Question 14

(das reduzieren des 'stocks' war falsch, fällt mir momentan auch grad nicht ein)

-> ich hoffe ich schreibe nicht nochmal deine alte version, aber ich denke schon, dass untenstehendes reduzieren stimmt

deliver
 any b where
  
 then
  
  selected := {}
 end

Question 15

deliver/GRD_INV_REF:

prp0_1: 
prp0_2: 
inv0_1: 
inv1_1: 
inv1_2: 
inv1_3: 
Conc.G: 

Abstract Guards + Modified Concrete Invariants erfüllbar

-> der (informelle) beweis ist für die invarianten trivial und für das stock(x) > 0 einfach (wobei man natürlich x:=b wählt)


Frage: auf der Reference-Card steht für "GRD_REF: Deterministic or non-deterministic but non-parametrized abstraction" dies ist jedoch bei uns der Fall. Ich habe deliver/GRD_INV_REF und deliver/EQL_REF (variable wird ja im Refinement wieder gebraucht) als Proof-Obligations gewählt. Keine Ahnung ob das sinvoll ist, nur so eine Bemerkung =). Würde dann so aussehen (hoffe ist richtig..):

(ich gebe dir absolut recht, mein GRD_REF war schwachsinn und nur das resultat einer verzweifelten suche nach einer zweiten proof-obligation ;) Incubus)


deliver/EQL_REF:

prp0_1: 
prp0_2: 
inv0_1: 
inv1_1: 
inv1_2: 
inv1_3: 
Conc.G: 
Gluing: 
  
Equality: 


Informaler Beweis: One can easily see that after applying EQL_LR for stock = stock1, MON and EQL the proof obligation is proved.

Hoffe hab nicht ein Schwachsinn geschriben =) Fabiom