Консультация 2010 (1185151)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Консультация к коллоквиуму по курсу «Формальная спецификация и верификация программ.Часть 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).

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов курсовой работы