Модели, исчисления и методы доведения индуктивных утверждений для эквациональных спецификаций с частичными функциями тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

1нститут мбернетики 1мен1 В. М. Глушкова АН УкраТни

На правах рукопису УДК 519.681

НАЙДИЧ Дмитро Едуардович

МОДЕЛ1, ЧИСЛЕННЯ I МЕТОДИ ДОВЕДЕНИЯ 1НДУКТИВНИХ ТВЕРДЖЕНЬ ДЛЯ ЕКВАЦЮНАЛЬНИХ СПЕЦИФ1КАЩЙ 3 ЧАСТКОВИМИ ФУНКЦ1ЯМИ

01.01.09 — математична жбернегика

Автореферат дисертацп на здобуття вченого ступени кандидата ф!зико-матеиатичних наук

Ки1в 1992

Робота виконана в ¡нституп к!бернетики ¡мен! В. М. Глуш-кова АН УкраТнн.

Науков1 кер1вники: член-кореспондент АН Украши, професор,

доктор ф!зико-математичних наук АНДОН Ф. I.,

професор, доктор техшчних наук КОВАЛЬ В. Н.

Офщшш опоненти: член-кореспондент АН Укра1ни, професор,

доктор ф{зико-математичних наук ЛЕТИЧЕВСЬКИИ А. А.,

кандидат ф1зико-математичних наук ДЕГТЯРЬОВ А. I.

ПровЦна уста нова: КнТвськнй полггсхшчний ¡нститут.

Захист вщбудеться « $ »—--о год.

на засщанш спещал1зовано1 вчено! ради Д 016.45.01 при 1нститут1 кибернетики ¡меш В. М. Глушкова АН УкраТни за адресок»:

252207 К"1В 207, просп. Академка Глушкова, 40.

3 дисертащею можна ознайомнтись у б1блютеш шституту..

Автореферат розкгланий « ^»

Учений секретар спешал1зовано1 ради

СИНЯВСЬКИЙ В. Ф.

1 - ' . » загальна !характп?>:стика роботи

Актуальн1ст' теми. ОстэниХм «асом у бэгэтьох га луз ян :;чуки 1 техн!ки впникэе потреба в програ>.пшя системах, крдтичшм ¿актором яких е над!'>.;иоть. ТрадицШ! «этодп забезпэчеккя иадхйкост! програм шляхом теотування вже не задовольняоть зроотапч! потреби практики. Внксристання ыов йормалькик спе:ш$1кац1й .1 нетод1в автоматичного доведения тесрец з Гфоаес! розр^бки ггоограм дозволяе досягнути якхоно нового ршгя у роэв'яташи задач! забезпзчення над1йност1.' Ц1 засоби доаволяють створовата точн! абстракта ! структурован! описи програм на ьс!;г етзпах розробки, тестувати .1 доводит« МдяоаШисть бьчыц детал1зованих опис!в опнсаы ветих р!гл!ь. Остание ззод:пься до доведешь твордж-нь, хстинних у стандартна модел! специф1кацП ярограми, - так звздих 1ндуктиБник касл1дк1в спеияф1кац11. Доведения зя1йс.кссться шляхсм побудови ЛОПЧНОГО виводу у Б!дпсыднсму чисяеян!.

Мови еквгшональних аягебра!чних спо^;1ф1клц1Г! сиочатку застосовуваяись для формал1зац11 абс-1 рактких ткгпв даних. За стаидартку модель спедиф1кацИ буз сбраний 1н1ц1альний об'ект категор!I II ыоделей. Г1от1м з'ясуваяась Э1дпов1д:псть мов алгебр Лчних сп«циф)кад!й до задач! "оказово над1йно! роэробкк програм. В рамках алгебраГчного п1дходу трансформацП даних, эд1йсноЕан програмаш, описуптьсл фушиЦями. - 0ск1льки тан! трансформацП в загальнсму виладку е частковими, наявн1сть засобаз опиоу часткових функц!й робить мову спецнфжаиДй б1льш адекватною до вказако! задач!.

Практична • застосування ков специф!кац1й для докагово над1йно! . розробки програм ¡¡ов'.-тзанс! касамперед з • розвптком в1дпов!дшх эасо<Яз доведения. Виоко, вю ь эагальному випадку мнохика 1ядуктизних насл!дгдв еквсипонально! специфакацП Сз частковими функциями) ке о рекурсивно перел1чимою. ВнаслЦок цього не !снуе ун1версального методу доведения таких твердасень. Окр!м того, рхьень азтоматизованост! Лснуючих метод!в доведения с недостатка. Тому задача розробки ксвих високо автсматиэованих метод!е доведения ¿ндуктивних насл1дк1в екэац!снальких специф1каиий з частковими функциями с. актуально».

Мета роботи - рсэробка нових метод!в догедекня пмуктивних насл!дк1в еквац!ональних спецификаций э частксьими функц!ями.

Роза'юаяля aiel задач! насловаио :<« дсслхдленн.' вяаставостей ¿пОДадышх кодэлей- таких спэциф1кац15 i poapcdai чисяеяь для доведения гвердхэкь, ютнкних в iKiuianbiiiö uozr*ii.

Наумова новизна 1 основ к i результата роботи. Шдх1д до специфдкгцП часткових функйй, виксристашШ t дисертацП, с уэагальн&миям багатосортно! еквац1онэльно1 лог1кк. При цьому п1дход1 отрога тэтсхшсть часткових функидй не кожэ бути виражена в мов1 тотогл^стей. В дисертацП запропокоьако поширення 'еквшионально! мови споци$1кац1й поняттям Ок-^отожностч, що узагальнюе понлтгя totoxhooti i дозволяе виразити строгу •готокн 1сть часткових фушаий.

Шохина 1ндуктивних иасладклв спемЗикацП кистить в codi шохику И логхчяих наел шив - твердкэнь, 1стинних' в yoix моделях спевдф1кацП,' Б ¿uicepiaiii I запропоковано числения для доведения лог1чшп: нася1дк!в. Розглянуто/ практично вахливий клас нормалышк сигнатур, Boi алгебра яких - масть непуст! Hocil. Сформульован! правила виведенкя тотохностей з акс1ом-тото&ностей i правила ьиведення Ок-тотожлостей э акс1ом- Ок-тспйжностей. Доведено теореки.про несуперечн!сть i повноту обозе чиолень иодо класу всix моделей специ$1кац!1.

ОперацШга семантика «квадхональних специф!кац1й базуеться на системах перешюування терм! в (СПГ). Вападок, коли специф!кацП виповддае канонМяа ОПТ, е детально- дослижеиим. Однак спецификациям часткових, функиЛй можуть в1длов)дати неньотеров! СПТ, по припускать незавершен1сть процесу отчисления деяких эначень функцп, В дисертацН досаддауеться послабления властивост! ньотерозсстх для канондчних СПТ. В звязку о цим для С1ГГ визначаеться властив!оть кваз1ка«он1чнсст1. Для КЕаз1какон1чяих СПТ еизнэчэно поняття алгебри кваз1нормальник форм. Для специфИсацИ, як iß в1епоь1дэс квазiканон1чиа СПТ . доведено твердаекня про • 1ьоморф1эы II 1нШ1ально1 модея! i ад эбри кваз1нормальш:< форм. Для алгебри кваз i норма л ьк их форм наведено вирдшиму достатню умсьу crporocTi антьрпретаиП функцдоналыш симьол1в. . .

Важливим класом ОПТ, що визначаеться i досдддяуеться в дисертацп, е клас деф1нцЦй. Визначальна умова для дефднШх вир!ши«а. Показало, що'деф1н1ц1я стакор.ить кваз1канондчну мноышу правил. Для мшацаоналышх специф!кэц1й, яккм вддловддають

де#1и1ц11, эапрояоноваьо два чися»лш типу пог.огтхтг для доведения 1ндукгпанях нао;адк13 - Ок-тотрхчоетей. , Принцип Ибе»{идукц,1йш>1 ядукцП", ' i якойу базовая! tu числения, вязначае ix високу а&томатизован1сгь. 0соблие1сть u:ü: числеиь полягас у BiscyTHocTi HboTeposocTi вшюйе;ш,<: 1кдукцП,- в;о використовуеться для !х обгрунтувакня. Наводиться приклад використання роэроблених чисяень для верк$1кацп елециркацП комп!лятсра просто! процедурно! мори.

Для канон!чких CI1T запропоновано числения 1ндуктивного поповн-ння без новдач!, поине в1,спов1дко до "спростування. 0соблив1сто цього числения с в!дсутн!сгь сблежень на редукцИз, властивих аналог!чним чясленням. Розв'язако задачу встановлення з^'яэку ць^о числения з поширення« чнсдення предикат! в первого порядку правилом !ндухщ1.

Практична значения. ; Результата лисертацП можуть оутк застосован! при створешй автоматизованих систем доведения теорем, но вмкористовувться для анал1эу епециф&ацМ. Запропонован! в дисертацП числения були застссовэя! в 1нстятут1 кибернетики 1м. В. М. Глушкова АН Укра!ни в рамках теми ДКНТ Украши "Розробка методов i засоб1в доказового проектування складнях програмо-апаратних систем на баз! лен .ко-алгебра!чного п1дходу".

Апробац!я роботи. CchobhI результата дисертацП були наведен! на сем!нарах Робочо! групя з компьютерно! анал!тнки (Ки!в. 1989, 1952), II Воессоэн!» конференаИ з штучного хнтеяекту Шнськ, 19SC), конференц!i IMACS з мояэлввання СЕэердом, Венгр1я, 1990), ШжнарсдниС л!тн!й школ1 э доказового проектування .прегрэм (Марктобердорф, Герман!я, 1992), Mi*pecny6jjiK£tfcbkiü кокференцП з математично! лог1ки (Казань, 1992), а також на каукових ceMiuapax Институту к!бернетики iM. В.И. Глушкова АН Укра£ни, факультету к!бернетики КиГвського университету, Обчислова.чьного центру АН РФ.

Структура роботи. Дисертац1я складаеться з вступу, чотирьох роздШв, зак!нчеиня, списку л!тератури I додатку.

ЗМ1СТ РОБОТИ

Перший розд!л присвячено вступу до теорП екваа^оналышх

сгецк$1кэц1Я s часгг.оьика; фунхц!л;да i poapodui чиолень для доведены* лоПчних Н2сл1дк1г> таких епещ;фгкй[Цй.

• В i 1. i вшсладзн! оскоеи теорП еявац10наль..лх специф1кац1й з частковими фукшаями, головною 1деев яко! е коделсвання часукоакх фуикцАй тотаяышмя. Ця теор!я с узагаяьпеишш сЗагатосортко! еквацюнально! лсг1ки.

ЗапроЕад'йея! надал! лоняття в1др1зняються гЛдкресленням. Часткова сигнатура г, - це багатосортна сигнатура, в як1й Ыдохремлен1 дежх футшонглън! ствола 2f\ 2- лгебра А являе собою багатосортку Е-алгебру, в як!8 в1докремяена тдаягебра А^ сигнат' ">и- 2+. Д-гомоморф1ам А->В - це багатосортний Е-гомоморфизм, шо е такоа Е+-гомоморф1змом А+->В+. 2Ь1аок'орф1зм являе собой багатосортний 2-1зоыор$1эм, що е такок 2+Чзог,:орф1эмог.1 А+->В+. Е;,йстов;;а 1нтерпретац1я залроваджених понят така. Перерхз гранка ГнтерлретацП f^;An->A функционального символу f{S з мноаинов (А*) визначае графа; частково! функнП СА+)П->А+. Систолам з в!дпов1даэть .тотальш в цьому значенн! функцП. Символам з мохуть ' виповиЗти

часткоп! функцИ. Ел'-чеити aj=a\a+ в1дпов!дасть. ■ зьйстовно неозначэнкм результатам обчислення функцП.

Сергд перемШзих V сигнатури 2 в1докремлмзтъся перемиш! V^, значения ооЛнки яких в ä'/nb-rKiü 2-алгебр1 А заьзди повинно наяежати А+. Алгебра Е,У-терм1в "TCS, УЗ являе собою- багатосортну алгебру Е-терлай над перемйннкмм V, де TC£,V)+ Mi стать в coöi 2+~терми над переьанними V+. 0ц1нка 2, V-TepvciB в Е-аягебр! А визначаеться як единкй гомоморф!эм T(£,V)->A, ио продовауа оц!нку перемшшх V->A. Постановка визяачаеться як спинка перекинних в алгебр! терм!в. Такы* чинсм, VV с T(2.V) + для будь-яко! постановки сг, Поняття тототаост! i П истикност! визначаються по аналоги з багатосортним випадксм. 1стинн1сть тотозшост! 1нвар1антна подо i30>"ip$iswy. Категср1я моделей- детально! множкни 2, v-тотожностей Е мае Шцдальну модель KP, Як i в багатосортному внаадку. алгебра КЕ) хзоморфна фактору Т(Э/^ алгебри основних тсрм!в Т(2). по .кокгруенцЦ породнено!

тотижноотями з Е. Б1лш точно, ^ - найменша конгруенц!я, то метить в codi Bei ucHOBKi приклади тотожностей Е; СТСЕ)/^)4 м i стить клас екв!валентности t_U основного терму t, акио tt,]f|t(d + i f. . ГквацДональна специ$1кац1я являе собой .'fpitoy

о

(Е,У,Е), ш позпачачться просто 3. Аягефа КЕЗ ьиЗчрасться за стаядартку модель спештф1кр,:х,11 Е.

Поняття ¡равчла п-3 репке/вання иизкачасгься по аналоги ч багагосортяим впаадко«. Систгт переписуганяд яряяс собес

тр!Яку С2, V, П), де К - Шохина 2,7-оравал перглиоуиаяня, 1 псоначаеться просто 8. В].тноценкд переписуулязя _|5>, вШозХдке до Р., визначаеться по аналог!I э багатоеортаим випадком. До класвч«»;« властивостеА кокфлюентноот! 1 кьот^рэао.Л додасться влгст»в1сть з(5<?Р1 гания над Шах тары1п. Правило 1->г з6ер[гае над!йн1 терки, якиэ з 1{ТСЕ,У) + впплкваз Ньотероза,

Сбасово) конфлоентва 1 збер1гяг/?а пал1йн! терми г/но дата правил називодться (с5азош) канонхчпоа. .Дяя' <5глово канон1чяо1 ьшсшлни Е,У-правил, позиачено! Р, по аналоги э багатосортким вяпядчоч ь-эначаеть^я алгебра н .эиальяих форм ТСР|^ , де ЦСТШ^) якщо 1(Т(а+. Алгебра ¿сокорфна '

В § 1.5 пропонуетьоя чксленкя для ■ дсведения лог!'¡них наол1дк1в аяге<5ра!чних спвци$1каи1й з частковимн фушшямн. Запроваджуеться п^ляття нормально! сигнатура - саг натура для яко! ТО^ * 0 для будь-якого сорту з. Фориул«з»ться правила виведення тотохностеЛ з акс!ом.

1=5 1--5 5=Ц

1) - ; 33 - ; ---;

1=1 5-1 ■ 1=4

45 ----а—а- ; 5) - .

ГСЦ.....____5П) Ь-эа

якцо 1=5 - гкс!ома, а ~ постановка. .. Наявн1сть виводу тотомост!. е з мнсжини акс1ом Е незначимо Е}-в. Нехай ЕИ> означаг лог!чнв сл1дуванн» тотохност! в з множини тдтожяоетей Е. -

Теорема 1. Нехай Е.е - тотожкост' нормально! -лигнатури, Тод] Е}-а тод! 1 пльки тэд1, коли Ер-е.

Поняття тото*лсст1 вчявляеться недостачньо виразним для формал1па1и х строго! тотожностх часткових функц1й. Тому мова слеииф1кацХй поширюеться пентттям 0к-тотожност1.

Для часткових фунишй /,§■■ Я->У чае ьисц? строга тотэжн^сть. якщо облает! виэначення цнх фуикц!й зб1гзиться 1 для ¿удь-якого кортеху гргумент!в х з облас.1 визначення / Сг^о ф /< х)х).

с£.У30к~ юто*н1егь - це пара вигл.яду СТ>_0Ие, де ЗТ -мкоуна Е.У-тершв, е - 7„ У-тотожн1сть. СЕ, У)Ок-тото';тсть

ЬТСОкЗ ti =12 е icwtimot' ь S-awjvtípi А, яьао для «5уд--яко! с Днки val:Y->A з того, до valCt.);/'' для eaix teST, внпйивас, ао vaL(ti)= vaíCtS). Э цього виэн&чэшш ькяливас, ,о т^тожн1сть е ыогша розгляцати як Ок-тото.тлхсть ü^Okle. ígthühíctI) Ок-тотоаностей ьмяьллст1>ся hmapíaimica подо Хзомор^зму.

Нехаи в алгебр! А визначеиа 1нтерпротаидя фунюиональшх символов fig, so в1д1юа!дае частковим функ'Цям / i g. Тод1 строга totosiiictb $ункц1й / i £ e¡ouвалентна ícthhhoctí в а ьаступно! пари Ок-тоюзаюсгой:

(f(v)>tOkJ'f(v)=g(v) i rgív3>[0kjfCv) =gCv), ке- v с V+, Ф"1муЛюаться -правила вш;адекчя Ок-тотояностей з аксиом.

ST[0kIt=t' STf0k3t=t' STÍOklt'4 1) -; 3D---; 3)

i)

STÍOfc]t=t ST£0kll'-i STC0kJt=t

ST(0)clt1=Sj,.; .„ST[Ok]tn=sn

БЪОкШ^,... Д^ГС^.... ,зл) - ;

, В правил! 5 терм;; сигнатури над перэышшш! С V, У")

розглядаютьоя як терки йагатосортно! сигнатури ' (Б.;1Э над П8реы1ннаки V, Нехай а - (Загзтозортна постановка 1 1егт~СоО= ■! Нзсгупне правило мае вигляд

5 )--:-:--, яйцо БТСОЮе - акс!сма;

БТоМе/п СсгЛОкЗеа

ЭТ.ГСЦ.....I НОкЗе . 8Т,у[0кЗе

6 )--4--0--, лад, ^Б4; 7)-----, ясао

БТ.Ц.....1п'[0к)е ЭТГОкЗе

¿ТГ0к]1=Г БТДЮкЗе Ь'ПОкЗе

8) -- ; 9)--.

БТДЧОкЗе БТДЮкЗе

НаяшЦсть вяеоду Ох-тотощгаст! ек з аксгом Ек поэиачико

-'^ай ЕкН>к оаначье логхчне ся!дуваиня 0к-тотсююст1 ек

& ннокинп Ок-тотожностей Ек.

Теорема 2. НекаЯ Ек.ек - Ок-тогохност! нормально! сигнатури,

Тог* ЕкН-'к тод! 1 т!- ',ки тод!, коли ЕкН?к-

Роздал 2 'прасвячеийй рсзроЗц! числень ш доведен" 1

Ок-тотожностей - хндултивнн:; насл1дк1в еквац!о.1:алыШ£

спецяфхкацхй б часткоьиии функциями.

Специф1кацдям багатьок зуЛстовнкл задач ь1дпов1дають <5азово

конфлсент(и система праы-ш, ао оОер;га»ть над1йн1 терми. Однак

ьластшйстъ ньстероьос?1 для таких систем може порушуватися

Такое, иаприклад, с мошша правил, цо м!стить ьизкачекня

s

секаптвки оператора циклу:

sokC ivhilei екрг, slm), env) = if svalC <?>rpr, envD / then seme vt'ioC expr, з*т!>, semi stri, env3) else env. D i Z. 1 досл1дхустьоя гсодэая (нШальио! ?'одел1, базоване на nepemscysaHHi терм1в, за ушви послабления властивосг! ilbcTopoBocTi. Природном послаблениям ньотеромсг! для базою конфлсентлмх 1. збер1гапчкх яад!йн1 терми многий Z, V-правия вияляеться вкмога ньотеровосг! вЦисиэння пэрегысування на T(E.V)+. Гак1 множини правил будемо назквати кеаз5канон штат. Для KB'siKanoHiuHoï мкбкина I. V-прзвил. назначено! надал! р, визначасться алгебра Кваз1нориаяьиих joga qt(d1î;. Поэначимо ЯогтЧк) шожину основных терм!в L, для яках { ТШ+. НеиаЛ <t> означав якщо ' ¿icrra+(s). i tj-клас сшивалентпсют! Ш. в алгебр! TOJ з прогиле&^му випадку. Визначимо

QTCDI " CQÎCIIiJK)+ = -СОТСОу" - CTCSVV":

2) f . ^t^.....<Ln» = <f(tj.....tn)>,

якщо ftSy s,_ vKsj,. ..snD i ijcTCSg tl<i<rù. Твердження Аягебри QT('¿Dц i ICR) e i30M0p<J«iiKa". В цьому параграф танож досл1джуютьс.ч достатн! умови конфлсентност!. Як 1 в багатосорткому випадку, ц! умсзи базовзн1 На понял! критично! лари правил. Сетевою уыоьок виявлясться властив1сть збер!ганяя над!йних терм!в.

Тверд»еняя 2. Нехай иножина правил R ньотерова, söepiras над!йи! терми i вс! Kpimrai паря правил П трив!альк1. Тоai мложина R е конфлсентногк

Твордгения 3. Нехай гагожяка правил R зберггас над1йн! терми i множииэ критичних пар правил Е порожня. Тод! мложина R е конфяюенткоп.

BarjiHBOD власти в i сто ^герпрэтац1 т функ'Цональних символ! в в часткових алгейрах е строг!сть, 2-алгебра А зветься строго», якщо для будь-лхого символу f<£ i кортежа аргумент!з â=(ajt... ,ап) з того, ш.о f/4ä)iA+, вшшгоас, ко А+ (Ш<п).

Формулсеться достатки умова строгоот1 глгобри QT(D|f. Множина Т„ l'-лразия Р зветься строгой, якдо л1ва частина будь-якого правила a R мае ьигляд fCtj,... .Ц), де tjtTCE.V)* С l<i<n).

Твердження 7. Нехай * е строгою множииоп правил. Towi алгебра QTdDL, е строгою.

В £ 2.2 запропэиовйНйй ¡летод доведения по 'ищуmil ittWHiiocTi Ок-тотогкоэтей в алгебр i QTCSH ¿я. Дик простота ьикяадсннл розглядэвться Ok-totcshoctí вигляяу tí Ote,1 е. Головка особл;®1сть запропонованого катоду полягае в псслаблешп для розглядувяного випадку ВИЫОГН HbOTCpOEOCTi вхдношэшш ОдукцИ.

Нехай dinapne вОновеняЯ OTCS.V) TCS, V) оадовольняе внмегак, позкачешш RESTR:

1) В1днош0ння < е замкнутом шодо множеняя на подстановку; 2} мдношенш < с яьотсроьиы на Nonr,+(tó,

Позкачимо Sub (Gsub) кножину (оскозних) пОстачовок. - Для терму ' позначного GS(t) мнохину осковних постановок y таких, ко tх í ИопаЧк). Мнохину подстановок Sub назвеыо ' <' -поу.риваючор для Ok-totoxhoctí UCkle, я'кцо для будв-якоо к Остановки r£SCt) оснувть постановки oeCov i y'£Sub так i, що l<Tf'<ly i GTCST тод! 1 Ti или тод1, копи QTC ¿D s ^oy1. Тод! наступив

правило ьквэдення (сформульовгаэ в ыетаыов13 suspiras остинность твердг.екь вОносно -QTCD^: 5

■■ptCav Cy'ífcSub (t(5<tcr * eko) i eka)

• ' ~ ek "

якщо C'ov - ' <' -пэкркьпюча ыногана постановок для ek=LÍGkJe. .При цьом; вОношения 1кдуки11 < не обоь'яэкоьо с ньотеровиы на TCL'.V). Узагадьнешя цього правила для множшш Ок-тотожностей Ек € таким. Нехай ek-Uük]e i ek'=lfOUe'.

-Vek^k ov'ek) fyek'eEk yá¿Sub Ct'iXtcr s e'ó) $ e&J qj.j¡))

yek^Ek ele

явде CovCek) - ' <' -покриваюча каокша nОстановок клл ektEk. Отасе, задача доведения (ПСО^ИЗс шже бути зведеиа до розв'яэання ьасгупних двох задач.

ЗАДАЧА 1. Вибрато вОвошення 1ндукцП <, що задоьояьняе уМОЕi RESTR.

ЗАДАЧА г. Запрспснуватя в и dip '<'-покриваючих млохия подстановок 1 ыетод доведения засиовху правила IKu

Б 5 е.3 фОксуються ckhtekchmhí умови, но накладаються на ыножииу правил i е достаткшл "для розв'язання поставдених задач. Ним умоьам вОпогОае поиятгя деф1н1ц.И. Основним змОтом moro параграфа е розв'язання аада-ri 1 для дефОШй. -Д^Ф.'.нпцею наливаеть^я множина Z.V-лравил R, для якс5 хенуг. под О на гпдмножиьи D«t(PJ i Fun (IR). що задовольняс наступним умовам;

1) якцс ].->гфаКЮ, то 1,геТС1:,У)+; I

2) ПаКЮ - баэово канонична шкшша .правил;

3) явдо 1->геГипСЮ, то ХеТСЕ.УГ;

4) ЕипСЮ - строга I збер1гапча над!.йя1 терми мьштна правил,

5) правила з Гип(!Ю не ма&ть критичних пар з Аншими еяек>?нтамн К.

Прикладом . дефШцП е мнскина правил, ао випорлдас специф!кацП комшлятора С роздал 3).

Показано, ш дефппцХя с кьаэ1канон1чкою шсхиноп правил. Ця задача вводиться до установления базово! конфлюенткост! дефШцП. . В1дм1тимо, цо достатт /ьювз кснфлюитясчл 1, дослхджен! в 5 2.1, на мохуть бути застосорат в цьо^у випадку. Теорема 4. Де$ .нШя е базсво конфлюеюто» «но*>:кос л-авил. Нехай из озяачае, що терм б € вяасннм гидтс-рмом терму I. Для мнояин» правил Я пооначико ^р тракэативяе замкн-эння вХднсшенн.ч (->р у ).). За иукане в1д!;о^оння 1ндуки,11 коке бути о^ран-е в1дношення

Теорема 5. Вшюшення задоволт "гае умов1 НЕБТС. Дозедення теорема поа'язано з застосуванням функцП "складност!" Моги+СЮ->На1, Еизначено! таким чином. Позначные СЬ(Ц мнозшну усгх ланцюгХв застесування правил з В? до терму I. Для терму 1еКогп+СЮ Позначимо мнохину вс^х панщепв

перепнеуваяня I в Еоэначкмо ШСсЫ порядков® число мнечлни застссувань правил з ГипСЮ а ланньгу сЬ. Визначи^о для 1#огга+(К), що ¿Ш^СсЮ, дэ сЬеСЬ^С^З. КсректШсть цьо'-о визначення внпливае з настулног твердження.

Тверджения 13. Якдо 1{Ноги','СИ, 1 сЬ'<ГЬ1(13, то

ЖсЮ<ШСсН'>. -

Властность строгост1 яеф1н1ци дозволяе зстгьорнти викснаняя умови КЕБТИ для в1днсыення де .ггаШльпс-

послабления деф1н.иЩ. НехаЯ Стаб1льне послабления

правила 1->г означав подстановку в правило' за?лсть южао! перем1кно1, для ...<о! число входхень в 1 не мелше *иж число В), дженъ в г. ново! переменно! з V".

Теорема 8. ¡Ндношення Хр, задоэояъняс умоЕам ПЕЗТЙ.

В § '¿. 3 розв'язуаться задача 2 а 5 2.1. За вилосч:ня 1ндукцЛ обнраеться ьидношеиня ^ . ¡Ькриравчэ

Ллдотановок вибирасться таким чином. Позначимо нзМ'ч:

гагапький ун1ф1катор терм1в t 1 s, Um] - фуккц!ональний символ,

е.? входить до терму t по ьходжеиню и. Нехай ш < <У означгс, цо

входження оз » власним идвходкекняк входження »'. Казне no

.циожянор суперпоаиц1йних постановок терму t по входженн» w

ыложшу SSCt.bO = < mguC ti ,, 1) ! w<w' & 3 r (1->г е Bö>.

Твердження 17. Нехай Uw]ç£~. То«1 множика SSC t, ы) с

fe -покривапчою для с1удь-яко1 0к-тотожност1, що мае вигляд

si ÜOkl».

Оинтакоичний характер офаного в!дношення ík .укцП д^зволке запропонувати метод отримання для кожно! тотожност! еег CtlOkleçEk, ceCovCtЕOk 1 еЭ5 ыножини Base(еоО приклад!в тотожностей вигпяду е'(5 СL't0k3e'eEJc>. кон'внкиЦя елеметчв яко! е лог1чнкм эасновком еа. При цьому гарантуеться виконання умоьи la j^^t'ó .

Нмсчв сформульован! правила виведэння пар <L,F> множив

Ок-тотожностей i поняття Eic-виводу для ыножини Ок-тотожностей Ек,

Mac mIctí наступиа теорема.

Теорема 9. Якщэ Ш - деф!н1ц1я нормально! сиГнатурк, то для

вс1х о<5'ект1в <L,R> Ek-вивод,, виконуеться наотупне твердження-.

для <5удь-дкш: ekçfc, açSSCt,ш), де UwJeZ", icHye с1мейство

Base( ek.tr) ¿.ц/Млдексованих kíhuóbhx множин п1дстаново1., >ао

задовольняе таким умовам: •

1) to t'd, якщо б ( BaseCek.cr).,,,, ek't Ш,

st ек

?J QTO^K & <■ 8 ek'« ) 4 eka,

sk'eLyR <5tBaseCek,er>e)c.

де ek=ttOkJe i ek^t'COkle'.

Cc'i jhhím елгментом Ek-виводу, згхдно з визначениям, е пара

<$, Ек>. Гакич чином, якцо iснус Ек-сив1д, то для Ек виконаний

засновок правила IND.

ГТерейдемо до формулсваиня правил виведення. Позначимо tñ-Ct.m)

множину fst'.O ! a í SSCt.w) & tar ->g, t'>. Us - тотожтсть t-s

aoo s=t. Hexafl EfJ — означав множику правил, отриману зам!нос

boíx перекйниж правил 0?, ко нал .ить до V+, ка hobí nepeiáHHi з

V*. Пару <L,R> позначимо L jj К.

L.ÜOkJe Я R

1)-------------------, якшо ttwJeE ;

t'.[ Ok) ou :<L'.ff>60à-Ct,o)D> ¡| R.ttOkîe

и

L.UOkJe jj R «

2 )---, якщо t py V\

¿,t' [Okie И R

L,tiOkJp=q ¡i R якщо t'[OkU=r(£ i I ± t'd

3) -:----,

L.ttOklptl<5<-rc5]=q || R ado

1i для Ecix vedomC<5) э viiTCS.V)" ышлтаае I £ vtf;

l.tiokjp=p i! R

4) -U_L_ .

I \\R

£k-: 1Водом мно.тани Ок.-тотожносте.. Ek наЗвеко ланцюг лосл!довних.эастосувгнь правил виведекня, перший елеис-нт якого ше вигляд <Ек,в>, a ocidimift - <j),Ek>.

Насл1дком теор"ли 9 е теорема про коректи!сть ч мления. Теорема 10. Нехай !R - дефШиЗя нормально! сигнатури. iCHye Ек~вив!д, то QTCDJRhEk.

В 5 2.4 пропонуеться ае одне розв'язакня задача 2. Нова полягае у використанн! специф1чно[ достаткьох умов» ¡.стинност! Ок-тотокност! в QTCDj^. Для П виклад°ння нам потр1б.чо ьиэначити нов! поляття.

Кожному символу Г & поставимо У BUIiOBiSHiCTb символ Г* Ti «I х apaocTi. Назвемо помдченос сигнатурою if псиырення сигнатури Г по«1чену.!«1 коп1ямн фушсц1ональвих сшаеся1з, ввазьапчк. в>,о ' Г*(С2*)+, якцо f£f npoe.KUiea псшченсго терму 1}'*Т( £*.'•.'> назвемо терм pr(t*){TCS,V). одержаний з I* усуненням hcmstok функдюнальних с яюл1в. Позначимо HOCl'b mhokihv щкшзяишх (по в1днов!енн» "бути пШхолкенням") пом1чаних вяодхень терму t;i. Часткова ясрмал1эаи1я £П: T(£*,V)->Т(E.V) ло>.иченого терчу оакачае ^-нормал^заци) проекций його п!дтерм!в по nciu мШиальшш пом1чеяим п!двходженняи:

pnCt*} * <Л «<- CprCtX))^]^^,,

в протилемюму вкладку результат pn(t*) не внэначений Правило переписувашш 1*->г* аветься 1й-кор<?ктним. ко п означаться i»-»r*. якщо д! • будь-яко! подстановки j-gGSiргС1*)) pn'.l'V) S> РпСгЛ ).

St

Твердзенкя 13. Якщо 1*->>г*, то QT( Dрг Q *) i Ok 1 рг С1 =рг С г .

Таким чиним, доведения ктинност! Ок-тото^чосгi HOj j 1 г мояе бути зведеие до доведения длл деякс! noui гки 1*,[ *

тершв 1,г Пропоковаааа метод дов-?д«аня К-коректносп dayуст ь;*

на »/1ря.уванялх. апаяэгдчних наведен»:м б § 2.1. При цьому ьикористовуеться дастатня умова К-п.оректносг1, пов'язана з гьреписуван ям ко.-Лчеких терм!в. Множима чксткк входжень C0(t*) гкниченого терм) I* кхстить такi його входгення ы, цо и i яке RcwiMsHe ьходгкшш и' терму L* не е гпдвхсдкенням w Ctm'<w). ¿удеио казати, цо ьходхеннк o¡ терму t* п; линуте, якцо воко не s 'п.о'пш. Множииу поглинутих входж&нь I* позначико S0CI*). Терм t*tT(£*, V) зветься схоьаним, ао поэначаеться Düd(t*), якцо для bcíx зходкень о э t*[«3ç(S*)~ випливае . Вкзначимо

вОншення поспа&геного пбрегсисуЕакня псшченкх терм!в: будемо писати íM->-psx, яхдо ^,<7 s* i IHidCvcri для bcíx переьинних

v.

- Твердження 50. Ято t*-> s* i правило р R-корек. то t*-»bx. ' Р

Для правила t,->s*. да WI'CE, VJ i s*<T(2*,V), назвемо миожмою суперпозиц!йяих »Остановок мкожину SS(t,w3, якцо будь-яке ¿ходжеиня и в терм s' переыОнсй, ег, эам1щу гься в яояк1й niдстаяо£ц! a 55(t,u), е поглипутим.

Сфоркулоемо правила виведення. Ой'екташ виводу е пари тоын лом1чеиих правил, но позначаються L || R. Для терму q почтачимо ¡nrkCq) терм, утворенаЯ э q помХткою головного фунмЦоналыюго символу q.

L,í->s* 3 R

1)-----якцо i[

¿,<t'-->sV : <t',cr>€ ¡R~Ct,w)} Il £,t~>s* i SSCl.u) - мнохтса суперпэзишйних постановок t->sK; L,t*-Ns* I) R

2) -' ü —г,- якцо де ugCOCt*) i ^Rií?, ;

¿..q ->s J R p-w SL

L,t*">sx J R якцо wíSOís*). prCs*|u) q.

L,tx->s4[oi<-ra-kCq3î | К ' -°rl~>r í!PTul l i для Ее i:: vçVardKVarCr) з '/с^Г( Z. v) ~ випливае t*j. ver; L t*->s* II R

4) _J--- . якцо pr(t*^pr(s*) i SOCl*)cSOCs*);

L й R

5) —V—=- , якт рг(1хЬ-рг(ск) i SOCt^cSOÍq*).

í..tj ->s |¡ R •

Г1 "биюдом mhckkshh .noMÍ4fei!Wi правил R1 назвемо ланцюг

^ослОопних эаетосуьань правил е,и ведения. перший элемент якого

мае вигляд <R1 ,0>, a ocranhiH - <0. Ri>t

Теорема 15. Якшо ioiiye Ш.-вивод, .to кохний елемент мюли ни R1 К-коректний.

В розд1л! 3 описаний приклад застосування розрсблених числень до задач! вериф1кацх1 спациф!кац11 компилятора. Специфшацдя Miстать опис процедурно! нови F1, абстрактно! машянн i перекладу олератор!в кови в коди машини. Р1 мхетить оператори привласнення, циклу та !х посл1довност1, а таз;о* предвязначен1 onepauii ..ад натуральными числами. Тото&ност1 э then_else

шделюються в специМкацП totoahoci ки з допомш^ши функцюнальними символами. Таким чином, множила правил, ь!дпов1дна до спец*(ф1кац11, вияаляеться дефипихе»- Семантика мовн визначаеться функцию 3en:Stm,Env->Env!, ew задач перетворения значень пэреьцкних Env в залежност! в1д оператор!? мови Stffi. (Знаком ! псзначаються фуямиональн! символа з ТГ i nepeMiHHl з V". 3 Семантика машини визначаеться фуцкгпео run:ListCode,Nat,Stack,En/->Env!, що эчдае перетворення значень яерем1нних в зал<здост1 в1д пссл1довност! код1в ListCode, зм1сту pericTpy Nat i стеку Stack, дкий ьистить посл1довност! ксд!в для .вкладенихЭ операторов циклу. Функцхя кошиляци соь.р: Stm-)ListCode визначае перетворення оператор]в SL у посл1доеност1 машинних код1в.

Умоьи коректност1 ксмлдляц!! виражен! тверд.тснням про icr/HHicTb в ста. ,apTHift шделх описано! спец.иф1кац11 назтулно! пари Ок-тотожностей:

semC s, e)[0k]sem( s, е) = run( compCs), 0, вир, е) i "'inCcompCs), р erap, e)C.Oic]sem(s,e) - runCcompCs"), 0, emp, e),' де. s:Stn i e.Env - nepeMiHni, 0: Mat i emp: Stack - початков! значения в!дпов!дно pericTpy i стеку.

Доводиться таке узагальнення них Ок-тотожностей: seraC s, еН0к!гш( lc, n, stk, semis, е)) =

runC comp(s)л1с, n, stk, e) i runC compCs)'Nic, n, stk, eMOkirunC lc, n, stk, senfs, e)3 =

runt comp(s)~Ic, n, stk, e), де n: Mat i stk: Stack - пэрэмши i ListCode, ListCcde-> ListCode - фушиля коккатенапП списков KOfliB. Доведения для друго! 0к-тотожност1 эводиться до доведения £Р-коректноет1 правил--» runC corap(s)'lc, n, stk. e) -> runC lc. n. stk, sem*(s. e))

Розд1л 4 MicTüTb чи.олэния типу пополнения для доведения тотожностей - ¡кдуктивник насл1л;к1в еквац1ональвих теор!й Каведегю нгобх1дн1 Еизкачення. Терм I називаоть ищуктнвно переписуваним множикою правил R CIRCO). яквд кожний ооновний приклад t може- бути переписаний правилами о R. Тотожн1сть s=t зветься iH^vKTHBHQ переписуванор множимо*) правил R CIR(s=t)3, якка одна з частин будь-якаго основного прикладу s=t, ¡но не е граф1чнои тотожн!стю, може бути переписана правилами з R. Тотожн1сть s-t эзеться доказово суперечною CPCCs-')), якто або не IR(a=t), або IRCs) 1 Ks для вибраного упорядкування <. Доказова c}iiep84hictb тотокностей вир1шнма. Спронуючим упорядкуванням зваться ньотерове упорядкуваня таке, но з s<t випливае uisKuiU i scKtc, а також з s>-t випливае s>t,

Нехай L - множина тогояюстей - 1ндуктиьких насл!лк1в R, < -слроцуюче упорядкування таке, ш,о с Нехай Л,В - ыножини ютожностей, CPCs->t) - множина критичних пар, , отриманих супг-рп0зи1пями правил з R усе^дину правила *->t. Ht ай sjt оэначае незр1внян1сть sit в'дносно >, А Ц В - пару <А,В>. В 5 4.1 сформульован1 правила виведення;

A,s=t |j В

1) -■--, якто t<s i IRCs);

A,CPCs->t) й В,s=t

A,s-t 8 В

2) - . якцо sill IRC.=t);

A.CPCs->D,CPCt->s) И B,s=L

A.'s-t Ц В якщо (га < 1а) i або a) l^rtCR U L)

3)

4)

A,s(ia<-raJ=t || В або 6) i*r e CA U B) i IRCs);

A.stla)=strcrJ [J В

А 8 В ' g-, A's=s 8 0

якщэ 1=г € (L У А У В); А Я В

Теорема 13,

1) (KopeKTHicTb.) Яхщо <А,0> ><3. В>, то А - множина ¡.ндуктивних

наслгдк^в R. .

2) СПовнота спростуваиняЗ НехаЯ R - баэово конфлсентка множина правил. Тол1 якцо деяка тогомисть з А не- е хкдуктивним наслхдком

ТО <А, {"'К'А',Б'> ДЛЯ ДеЛКИХ МНОККН А', В', таких, но к' MiCTHTb

док^аово супрречну юто.жшсть.

3) CBijicyraicTb невдачьО Якщо до napfi <н,В> н<- можна застосузага н!якого правила, то А - кнопша доказово суперечни:; тотсясносте.Ч.

BífluiTHMO, що в аналбг1чяих чясленнях умова застосувзння правила 3) м!стить додаткове оСиезкення: s >• lor ado 1>г. Однак при цьому умова застосувгшя правила 1) с сйльш rara ль ною: IRCs3 i tCL>s). Виявляеться, що зберОання niel умом при усунешп вказаного обмеж.ення на редукцш приводить до порушення коректностi числения. Наприклад, нехай R={fC0)=0, fCsC;0)-f(x3, gC0)=l, c{sCx))=gCx)> Пехай такок f(x), Cx)rigíC >f(03. Тод1 о fCx)=g(x3 застосуванням "послаблоного" правила 1 породжуегься tototjíoctí f(x)=g(sCx)I i 0=g(0J. Обидвх totoxkoctí поглинаються. причоыу друге - нля^м яастосуванкя правила g(0)->fC0) до т^рм/ gCQ). Таким чином, доводиться тотоюйсть, ао кэ с ондуктивним наслОком R.

В 5 4.2 розв'язуетьоя задача ^становления взаемозв'яэку mí» запропоковажш численням та покшренкям правилом ондукцП прямого аналогу числення предикат!в поршого порядку з тотеяшстю C'-ífD. Особливость аього числения полягае лише в о бмеже:;^ па постановку замють перешнних V+ термов ТСЕ, V3+. За визодим! $ормули достатньо розглянути умовн i TOTOXHOCTi.

Hexafl CSCs-O означае CPCs-)D, якцо t<s. i CSfs-t) = CCPCs->U U CPCt->s)\ якшо s*t. Пехай CSC A)-- y<CS(e) ! ecA>. Позкачимо inaxCs=t) CminCs-t3) гаоашну ' <' -максимальних См1н0мальних) ел&чент1в множини Cs,t>. Позначимо <д упорядкуваннд мулмомножик, вОповОне до <.

Правило ОдукцП. Для множини тотожностей A i (СРСА)»А)-1ндексован01 лиожини п.Остановок 3ase

CL.J1)

СС а а e'er ) 4 е 3

е«СРСА) e'jA o'tBase(e,e'3

Je '

е^А

якщо для Bcix ееСР(А), еЧА, atBase(e,e'3

1) fCCe');'

2) або iraxCe'tr) <л naxCe) i minCe'o) <д niinCe), або для деякого терму тре ШтЗ i ¡гахСэ'сг) <т>.

Теорема 14. Hexafl тотожя1сть е виеодить'-я з aKcicM cííu'U ь числешй ЧП поширеним правилом INDI. Год? с - он^уктивтЫ насяОок К.

Теорема 15. Не::ай <А,р> f <fí,B>. Тод1 будь-яка тотскн1сть есЛ ей водиться з акс!см (Я U D в численв! ЧП поширеним правилом Ш1.

Ochobhí резуьтати дисертацП каведен1 в таких роботах: .

1. Антимиров В.М. , Найдич Д. Э. О частично упорядоченной и решеточной типизации // Математические методы управления и обработки информации. - М. : МФТИ, 1986. - С. 31-65.

2. Антимиров В. М. , ' Найдич Д. Э. Модели и исчисления для частичных функций // Тез. докл. VIII Сибирской школи "Программное обеспечение ЭВМ новых поколений". - Иркутск, 1989. -С. 102.

3. Антимиров Б.М., Найдич Д. Э. Алгебраические спецификации с частичными функциями // Сб. докл. II Всесоюзной конференции по искусственному интеллекту, -Минск, 1990.-Т.3, С.242-246.

4. ^.ntimírov V. , Najdich Г , Koval V.Partial fune*ions in simulation: formal models and calculi // Proc. IMACS Europían Simulation Meeting, - Egerdom, Hungary, 1990. - P. 133-137.

5. Коваль Ю. В., Найдич Д.Э. Автоматическое доказательство индуктивных теорем на основе индуктивного пополнения /v ^ещэкие задач на математических моделях предметных областей. - Киев: Институт кибернетики им. В. М. Глушкова , 1992. - С. 38-47.

Б. Найдич Д. Э. Индуктивное пополнение для э! национальных спецификаций с частичными функциями // Решение задач на математических моделях предметных областей. - Киев: . Институт клбернь.ики им. Ч. М. Глуш.кова , 1992,- С. 62-73.

7. Правило индукции для исчисления индуктивного пополнения .'/ - Тез. XI Мэжресл. конф. по математической логике, Казань, 1S92.. - С 102.