Розширення мови SIPL: Введення булевих змінних
1.6.1.
Синтаксис розширеної мови SIPL можна задати за допомогою наступної БНФ (див. Табл.1.4), доповнивши базову (див. п.1.1) новими правилами та розширивши існуючі з урахуванням нових конструкцій:
Таблиця 1.4.
| Ліва частина правила – метазмінна (дефінієндум) | Права частина правила (дефінієнс) | Ім’я правила |
| <програма> ::= | begin<оператор> end | NP1 |
| <оператор> ::= | <змінна_чис>:=<вираз_чис> | <змінна_бул>:=<вираз_бул> | <оператор> ; <оператор> | if<вираз_бул> then <оператор> else <оператор> | while <вираз_бул> do <оператор> | begin <оператор> end| skip | NS1 NS2 NS3 NS4 NS5 NS6 NS7 |
| <вираз_чис> := | <число> | <змінна_чис> | <вираз_чис > + <вираз_чис > | <вираз_чис > – <вираз_чис > | <вираз_чис > * <вираз_чис > | <вираз_чис > ÷ <вираз_чис > | (<вираз_чис>) | NA1_1– NA1_7 |
| <вираз_бул> ::= | <бул> |<змінна_бул>| <вираз_чис>< <вираз_чис>| <вираз_чис> £ <вираз_чис> | <вираз_чис> = <вираз_чис> | <вираз_чис> ¹ <вираз_чис> | <вираз_чис> > <вираз_чис> | <вираз_чис> ³ <вираз_чис> | <вираз_бул>< <вираз_бул> |<вираз_бул> £ <вираз_бул> | <вираз_бул> = <вираз_бул> | <вираз_бул> ¹ <вираз_бул> | <вираз_бул> > <вираз_бул> | <вираз_бул> ³ <вираз_бул> | <вираз_бул> Ú <вираз_бул> | <вираз_бул> Ù <вираз_бул> | Ø <вираз_бул>| (<вираз_бул>) | NA2_1– NA2_17 |
| <змінна_чис> ::= | M | N | . . . | NV1–… |
| <змінна_бул> ::= | M_B | N_B | . . . | NV1–… |
| <число> ::= | . . . –1 | 0 | 1 | 2 | 3 | . . . | NN1–… |
| <бул> ::= | true |false | NB1-NB2 |
|
|
|
В даному випадку множину всіх виразів розділено на булеві та цілочисельні. Введемо позначення для всіх синтаксичних категорій та нові метазмінні, що вказують на представників цих категорій (див. Табл.1.5).
Таблиця 1.5.
| Метазмінна | Синтаксична категорія | Нова метазмінна |
| <програма> | Prog | P |
| <оператор> | Stm | S |
| <вираз_чис> | Aexp | a |
| <вираз_бул> | Bexp | c |
| <змінна_чис> | Var | x |
| <змінна_бул> | Var_B | y |
| <число> | Num | n |
| <бул> | Bool | b |
В наведених позначеннях БНФ мова SIPL набуває наступного вигляду (Табл.1.6):
Таблиця 1.6.
| Ліва частина правила – метазмінна (дефінієндум) | Права частина правила (дефінієнс) | Ім’я правила |
| P ::= | beginS end | NP1 |
| S ::= | x:=a| y:=c| S 1; S2| ifc then S1 else S2 | while c do S | begin S end | skip | NS1 NS2 NS3 NS4 NS5 NS6 NS7 |
| a := | n | x | a 1+ a2 | a1 – a2 | a1 * a2 | a1 ÷ a2 | (a) | NA1_1– NA1_7 |
| c ::= | b |y| a 1< a2| a1 £ a2 | a1 = a2 | a1 ¹ a2 | a1 >a2 | a1 ³ a2 | c1 < c2 |c1 £ c2 | c1 = c2 | c1 ¹ c2 | c1 >c2 | c1 ³ c2 | c1 Ú c2 | c1 Ù c2 | Ø c| (c) | NA2_1– NA2_17 |
| x ::= | M | N | . . . | NV1–… |
| y ::= | M_b | N_b | . . . | NV1–… |
| n ::= | . . . –1 | 0 | 1 | 2 | 3 | . . . | NN1–… |
| b ::= | true |false | NB1-NB2 |
|
|
|
Надалі будемо користуватися введеними позначеннями для запису структури програм та їх складових.
Базові типи даних – множини цілих чисел, булевих значень та змінних (імен):
· Int={ . . . , -2, -1, 0, 1, 2, . . . }
· Bool={true, false}
· Var={X,Y, … }
· Var_B={X_B,Y_B, … }
Похідні типи – множина станів змінних (наборів іменованих значень, наборів змінних з їх значеннями):
· State={Var ®Int,Var_B ® Bool}
Приклади станів змінних: [Ma8, Na16], [Ma3, Xa 4, Yatrue, Nafalse].
Операції на множині Int. Символам +, – , *, ¸ відповідають операції add, sub, mult, div (додавання, віднімання, множення, ділення). Це бінарні операції типу Int2 ® Int.
Операції на множині Bool. Символам Ú, Ù, Ø відповідають операції or, and, neg. Це бінарні операції типу Bool2 ® Bool (диз’юнкція та кон’юнкція) та унарна операція типу Bool ® Bool (заперечення).
В мові також є операції змішаного типу. Символам операцій порівняння <, £, =, ¹, ³, > відповідають операції less, leq, eq, neq, geq, gr. Це бінарні операції типу Int2 ® Bool.
Крім того, введемо
· функцію-константу арифметичного типу 
: State®Int, таку що (st)=n,
· функції-константи бульового типу 
, 
: State®Bool такі, що (st)=true, (st)=false,
|
|
|
· тотожну функцію id: State®State, таку, що id(st)=st.
Отримали багатоосновну алгебру даних мови SIPL
A_Int_Bool_State =<Int, Bool, State; add, sub, mult, div, or, and, neg,
less, leq, eq, neq, geq, gr, Þ x, xÞ,Þ y, yÞ, 
, 
, id, Ñ, 
, 
>
Формули обчислення задаються аналогічно алгебрі A_Prog.
Нові правила побудови семантичного терму подано у табл.1.7:
Таблиця 1.7.
| Правило заміни | Номер правила |
|
sem_P: Prog ® FS задається правилами:
| |
| sem_P(beginSend)= sem_S(S) | NS_Prog |
|
sem_S: Stm ® FS задається правилами:
| |
| sem_S(x:=a)=ASx(sem_A(a)) sem_S(y:=c)=ASy(sem_B(c)) sem_S(S1;S2)= sem_S(S1) ·sem_S(S2) sem_S(ifcthenS1elseS2)= IF(sem_B(b), sem_S(S1), sem_S(S2)) sem_S(whilecdoS)= WH(sem_B(b), sem_S(S)) sem_S(beginSend)=(sem_S(S)) sem_S(skip)=id | NS_Stm_As NS_Stm_As_B NS_Stm_Seq NS_Stm_If NS_Stm_Wh NS_Stm_BE NS_Stm_skip |
|
sem_A: Aexp ® FA задається правилами:
| |
sem_A(n))= 
sem_A(x))=xÞ
sem_A(a1+a2)=S2(add, sem_A(a1), sem_A(a2))
sem_A(a1–a2)=S2(sub, sem_A(a1), sem_A(a2))
sem_A(a1*a2)=S2(mult, sem_A(a1), sem_A(a2))
sem_A(a1¸a2)=S2(div, sem_A(a1), sem_A(a2))
sem_A((a))=sem_A(a)
| NS_A_Num NS_A_VarNS_A_Add NS_A_Sub NS_A_Mult NS_A_Div NS_A_Par |
|
sem_B: Bexp ® FB задається правилами:
| |
|
sem_B(b)=
sem_B(y)=yÞ
sem_B(a1<a2)=S2(less, sem_A(a1), sem_A(a2))
sem_B(a1£a2)=S2(leq, sem_A(a1), sem_A(a2))
sem_B(a1=a2)=S2(eq, sem_A(a1), sem_A(a2))
sem_B(a1¹a2)=S2(neq, sem_A(a1), sem_A(a2))
sem_B(a1³a2)=S2(geq, sem_A(a1), sem_A(a2))
sem_B(a1>a2)=S2(gr, sem_A(a1), sem_A(a2))
sem_B(c1<c2)=S2(less, sem_B(c1), sem_B(c2))
sem_B(c1£c2)=S2(leq, sem_B(c1), sem_B(c2))
sem_B(c1=c2)=S2(eq, sem_B(c1), sem_B(c2))
sem_B(c1¹c2)=S2(neq, sem_B(c1), sem_B(c2))
sem_B(c1³c2)=S2(geq, sem_B(c1), sem_B(c2))
sem_B(c1>c2)=S2(gr, sem_B(c1), sem_B(c2))
sem_B(c1Úc2)=S2(or, sem_B(c1), sem_B(c2))
sem_B(c1Ùc2)=S2(and, sem_B(c1), sem_B(c2))
sem_B(Øc)=S1(neg, sem_B(c))
sem_B((c))= sem_B(c)
| NS_B_Const NS_B_Var NS_B_less NS_B_leq NS_B_eq NS_B_neq NS_B_geq NS_B_gr NS_B_lessB NS_B_leqB NS_B_eqB NS_B_neqB NS_B_geqB NS_B_grB NS_B_or NS_B_and NS_B_neg NS_B_Par |
|
|
|
Приклади розв’язків задач.
Припустимо, що у SIPL введено лише базові необхідні предикати: Ø, Ú, £. Виразимо решту предикатів Ù, =, >, ¹, <, ³ через базові: у змінну res записати результат обчислення відповідного предикату над значеннями вхідних змінних A та B.
Завдання 1.7. Розписати Ù через Ú і Ø .
begin
if 
then res:=true
else res:=false
end
Побудуємо дерево виводу:
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=IF(S1(neg,S2(or,S1(neg,A=>),S1(neg,B=>))),ASres( 
), ASres( 
))
Доведемо часткову коректність:
Маємо початкове дане d=[A 
,B 
].
Sem_P(P)(d)= IF(S1(neg,S2(or,S1(neg,A=>),S1(neg,B=>))),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
= 
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Завдання 1.8.Розписати = через ≤
begin
if 
then res:=true
else res:=false
end
Побудуємо дерево виводу:
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=
=IF(S2(and,S2(leq,X=>, Y=>),S2(leq, Y=>, X=>)),ASres( 
), ASres( 
))
Доведемо часткову коректність:
d=[X 
,Y 
]
Sem_P(P)(d)=
=IF(S2(and,S2(leq,X=>, Y=>),S2(leq, Y=>, X=>)),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Завдання 1.9. Розписати >
begin
if 
then res:=true
else res:=false
end
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=
=IF(S1(neg,S2(leq,X=>, Y=>)),ASres( ), ASres( ))
Доведемо часткову коректність:
d=[X 
,Y 
]
Sem_P(P)(d)=IF(S1(neg,S2(leq,X=>, Y=>)),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
=
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Завдання 1.10.Розписати ≠
begin
if 
then res:=true
else res:=false
end
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=
=IF(S1(neg,S2(eq,X=>, Y=>)),ASres( ), ASres( ))
Доведемо часткову коректність:
d=[X ,Y 
]
Sem_P(P)(d)=IF(S1(neg,S2(eq,X=>, Y=>)),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
=
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Завдання 1.11.Розписати <
begin
if 
then res:=true
else res:=false
end
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=
=IF(S2(and,S2(leq,X=>, Y=>),S2(neq, X=>, Y=>)),ASres( ), ASres( ))
Доведемо часткову коректність:
d=[X ,Y ]
Sem_P(P)(d)=
=IF(S2(and,S2(leq,X=>, Y=>),S2(neq, X=>, Y=>)),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
=
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Завдання 1.12.Розписати ≥
begin
if 
then res:=true
else res:=false
end
Побудуємо семантичний терм:
Sem_P(P)=Sem_S(if then res:=true else res:=false)=
=IF(S2(or,S2(gr,X=>, Y=>),S2(eq, X=>, Y=>)),ASres( ), ASres( ))
Доведемо часткову коректність:
d=[X ,Y ]
Sem_P(P)(d)=IF(S2(or,S2(gr,X=>, Y=>),S2(eq, X=>, Y=>)),ASres( ), ASres( ))(d)=
= 
=
= 
=
= 
=
= 
Часткову коректність доведено.
Програма не має циклів, тому вона завершується. А оскільки часткова коректність доведена, то маємо тотальну коректність.
Дата добавления: 2018-04-05; просмотров: 371; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!