Консультация 2010
Описание файла
PDF-файл из архива "Консультация 2010", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Консультация к коллоквиуму по курсу «Формальная спецификация и верификация программ.Часть I. Спецификация программ»20.10.2010Билет № 1ФИО:____________________, группа _________, бонус___Дать эквивалентное implicit-определение функцииОтвет:variable x : Intvalue f: Int -> write any Unitf(t) is ( if x = t then x := t end )1.
«Неазартное 21» : Задача системы - визуализировать поле игры (Game) и модифициро-вать его в ответ накоманды игрока. В колоде 36 карт (вальты, дамы, короли, тузы, 6-ки, 7-ки, 8-ки, 9-ки и 10-ки четырех мастей);стоимость карт: валет - 2, дама - 3, король – 4, туз – 11, 6-ки–10-ки имеют стоимость, соответствующуюсвоему названию. Банкир (Banker) играет с единственным игроком-соперником (Gambler). Сначала игрокберет из колоды (PackOfCards) себе карты (набирает свой Hand), затем банкир берет из колоды себе карты.Если сумма набранных баллов по картам у игрока равна 21, он выиграл; больше 21 – проиграл; иначе если убанкира 21, он выиграл; если больше 21 – проиграл; в противном случае выигрывает тот, кто набрал большуюсумму баллов.type Token, Card = Token -m-> {| n : Nat :- n isin {2..11}\{5} |},Hand = Card-set, Banker = Hand, Gambler = Hand,PackOfCards = Card-list, Game = Gambler >< PackOfCards >< Bankervalue newgame : Unit -~-> Game,-- если карта берется, то в случае gamblerMove она переносится-- из PackOfCards в Gambler, в случае bankerMove – в BankergamblerMove : Game >< Bool -~-> Game, -- 2-й аргумент-прекращение выбора картbankerMove : Game >< Bool -~-> Game, -- 2-й аргумент-прекращение выбора карт2.
Определить, противоречива ли данная алгебраическая спецификация. Ответ обосновать (доказатьпротиворечие или привести модель спецификации в доказательство непротиворечивости). Считать, что вовсех типах есть достаточное количество различных значений.type Place, Name, Volume, Info, DBvalueempty: DB,free: DB >< Place -> Bool,make: Name >< Volume -> Info,name: Info -> Name,volume: Info -> Volume,add: DB >< Place >< Info -~-> DB,get: DB >< Place -~-> Info,update: DB >< Place >< Name -~-> DBaxiom forall db: DB, pi, p: Place, info:Info, n: Name, v: Volume :-free(empty, p),free(add(db, pi, _), p) ispi ~= p /\ free(db, p),name(make(n, _)) is n,volume(make(_, v)) is v,get(add(db, pi, info), p) isif pi = p then info else get(db, p) end,update(add(db, p, info), p, n) isadd(db, p, make(n, volume(info))),update(add(db, pi, info), p, n) isadd(update(db, p, n), pi, info)3.
Существует ли модель, отвечающая приведенной спецификации, чей конечный автомат содержал быпредставленный в задании подавтомат? Ответ обосновать (доказать несуществование или привести модель вдоказательство существования).type E, Svalue empty: S, add: S >< E -> S,tail: S -~-> S,include: S >< E -> Boolaxiom forall s: S, e, e1: E :tail(add(s,e)) is s,include(add(s,e1),e) is e = e1 \/ include(s,e),~include(empty,e)add(*,e1)ad add(*,e1)d(*,e2)Примечание: оформлять ответ к задаче №1 на отдельном листеadd(*,e2).