115 lines
5.2 KiB
Markdown
115 lines
5.2 KiB
Markdown
https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpJ4Recall1the4officeyassignment%2F4puzzle2from3Fichaz17r3whereBHz44people1areydistributed%2F0byz35officesl2such2that7vH7s2each4person0is6assignedza4singleVHm2Nuno1and3Pedro0do1not3share0anlHl0If1Ana1hasoo2just1for5herselfV2then0so2doesdHg5Officesyaccomodate%2F0at2most1twouIHHuBuMg0if5running2Why32withXyappropriate%2F1SMT4solverlBH0inuByfollowing%2F1you2will0be2able0to5inspect5counterASA6examplesBH2when6adequate7tBNHHz1s3Modele5problemuI6definingVVypredicate%2FBKuQ5writingza1set0of4axiomsfH0In3orderV5expressc3thirdyrequirement%2F3above7r4defineBHfc7h3alonesyexpressing%2Ful5someoneuMg2onlyBH6occupierXSuVWHEz2s2ShowikTuGuPyinconsistent%2Fu0u3hBKu12goalhHEz3s2Find1outuhfunyproperties%2F4followuDpb7vL7suP3MariaPuKR1One7ruT1sheukukLfu7u7u7u8iTDccuOusuLuMu9lbbXmuSaBL5equally2haveusiiidBMDHz4s5Finallyfyformulate%2Fg3provezau85statingVBLuUuU1onef1mayvG3emptyd1For2thisc3first3writeduvBHuwdVfvAg7nzieAzesuzu%2FvO4anyone7ItBHDz5n5Producefyalternative%2Fyformalization%2F3usingV5insteadvEVVpBLr3logic6functionU3givesvB4uniqueRXXBHuIuIY4Repeat1allk6previous3stepsuXvWVlDN7JoBNNNN4moduleuQNF2typec7yu7781Twos3ThreeHnanu%2Fou%2FsvBsvANHveyhasOffice%2F7nk7orerNH3axiom0A1B7v4forallzprAlV4existszopAjphmoHj0A2BmjorAj7r0o10o2BphhJhln7O3qqm7MzoUqFHfzBBiBfnoqhhiVngqUlgLo7RzqDHVurUbfAZUZbWAoAaap0p1plpJjbikiapkpbngpNFXzCgdPlrWHnzDBnBbk0p20p3ApZRdqXXJakoZqjqqqjqdLnam7XuqqnqsrpNMBvHysanity%2Btest%2Fg3falseuAA3checkuzvk3model3makes3senseAvpHHi0g1BiBZvvvrYv3qHm0g2mPvyrQQ7nhv1nOqvxq7oeBLvvvxAhAhhkvyoiqcqBNDvxvQdzoiif7yazpAoAvxdvQjenijHH3lemmayatMostOneEmpty%2FBjBiXcqBegdoarnXLpbqNN1endBNNNNvnyOffices%2BFn%2FBNDvqinv978vosvoHnTnv%2Bov%2BsOsONHvZhPkSVBpNHvqzBqqjvprhHHv8v4izplAhhcOzooAi7tpvpplpJqfjOlrqrpHFbzCkeWkraNHnzDnBfkvrvqpddoAeAnv8qAqAmqpAqAqgLdnprovprpBpBrnNNDv0vpBhBvpBNHqvxBqnOUv9fXpHlvxBllVkrOkrlprUNHOv27nOiAn7olRzpAoAQQmpUkHHv0v0Blkv0v0qkjeov8rnZLpeqNNv0NNNN
|
|
```c
|
|
(*
|
|
Recall the office assignment puzzle from Ficha 1, where
|
|
4 people are distributed by 3 offices, such that:
|
|
- each person is assigned a single office
|
|
- Nuno and Pedro do not share an office
|
|
- If Ana has an office just for herself, then so does Pedro
|
|
- Offices accomodate at most two people
|
|
|
|
Recall that, if running Why3 with an appropriate SMT solver,
|
|
in the following you will be able to inspect counter-examples
|
|
when adequate.
|
|
|
|
|
|
1. Model the problem by defining an appropriate predicate
|
|
and writing a set of axioms.
|
|
In order to express the third requirement above, define
|
|
a predicate "alone" expressing that someone is the only
|
|
occupier of an office.
|
|
|
|
2. Show that the axioms are not inconsistent by writing an
|
|
appropriate goal.
|
|
|
|
3. Find out if the following properties follow from the axioms:
|
|
- If Maria is assigned office One, then she will be
|
|
the only occupier of that office.
|
|
- If Ana and Nuno share an office, then Maria and Pedro will
|
|
equally have to share an office.
|
|
|
|
4. Finally, formulate and prove a goal stating that
|
|
at most one office may be empty. For this, first write a predicate
|
|
expressing that an office is empty (i.e. not assigned to anyone).
|
|
|
|
5. Produce an alternative formalization using, instead of a predicate,
|
|
a logic function that gives the unique office assigned to
|
|
each person. Repeat all the previous steps with this formalization.
|
|
|
|
*)
|
|
|
|
|
|
|
|
module Offices
|
|
|
|
type office = One | Two | Three
|
|
type person = Ana | Nuno | Pedro | Maria
|
|
|
|
predicate hasOffice (person) (office)
|
|
|
|
axiom A1 : forall p:person. exists o:office. hasOffice p o
|
|
axiom A2 : forall p:person, o1 o2 : office.
|
|
hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
|
|
|
|
axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
|
|
o1 <> o2
|
|
|
|
predicate alone (p:person) = forall o:office. forall p1:person.
|
|
(hasOffice p o) /\ hasOffice p1 o -> p = p1
|
|
|
|
axiom C : alone Ana -> alone Pedro
|
|
axiom D : forall p1 p2 p3: person, o:office.
|
|
hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
|
|
p1 = p2 \/ p1 = p3 \/ p3 = p2
|
|
|
|
goal sanity_test : false (*check if the model makes sense*)
|
|
|
|
goal g1 : hasOffice Maria One -> alone Maria
|
|
goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) ->
|
|
exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2
|
|
|
|
predicate empty (o:office) = forall p:person. not (hasOffice p o)
|
|
|
|
lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
|
|
o1 = o2
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module Offices_Fn
|
|
|
|
type office = One | Two | Three
|
|
type person = Ana | Nuno | Pedro | Maria
|
|
|
|
function office (person) : office
|
|
|
|
axiom B: office Pedro <> office Nuno
|
|
|
|
predicate alone (p:person) = forall o:office. forall p1:person.
|
|
p1 <> p -> office p <> office p1
|
|
|
|
axiom C: alone Ana -> alone Pedro
|
|
|
|
axiom D: forall p1 p2 p3: person. p1<>p2 /\ p1<>p3 /\ p2<>p3 ->
|
|
office p1 <> office p2 \/ office p1 <> office p3
|
|
|
|
|
|
goal sanity_test : false
|
|
|
|
goal g1 : office Maria = One -> alone Maria
|
|
goal g2 : office Ana = office Nuno -> office Maria = office Pedro
|
|
|
|
predicate empty (o:office) = forall p:person. office p <> o
|
|
|
|
lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
|
|
o1 = o2
|
|
|
|
end
|
|
```
|
|
|
|
|