Розширення мови SIPL: Введення викликів функцій

Подамо у наступній таблиці (Табл.1.8) cинтаксис розширення БНФ:

Таблиця 1.8.

Ліва частина правила – метазмінна	Права частина правила	Ім’я правила
<програма> ::=	…\| program <списокоб’явленьфункцій> begin<оператор> end	NP1 NP2
<вираз> ::=	…\| if<умова> then <вираз> else <вираз> \| <виклик функції>	NA1–NA7 NA8 NA9
<списокоб’явленьфункцій>::=	e \| <об’явленняфункції> \| <об’явленняфункції> ; <списокоб’явленьфункцій>	LDF1 LDF2 LDF3
<об’явленняфункції>::=	func<ім’я функції>=<вираз> \| func<ім’я функції>(<списокформальних параметрів>)= <вираз>	DF1 DF2
<ім’я функції> ::=	<змінна>	NF
<список формальних параметрів>::=	<змінна> \| <змінна> , <список формальних параметрів>	LFP1 LFP2
<виклик функції> ::=	<ім’я функції> \| <ім’я функції> (<список фактичних параметрів>)	CF1 CF2
<список фактичних параметрів>::=	<вираз> \| <вираз> , <список фактичних параметрів>	LAP1 LAP2

Тобто ми змінили синтаксис виразу: додавши варіант завдання виразу за допомогою умов

<вираз> ::= if<умова> then <вираз1> else <вираз2>

якщо умова виконується, то <вираз> := <вираз1> інакше <вираз> := <вираз2>, або ж

<вираз> ::= <виклик функції>

значення виразу буде дорівнювати результату виклику функції.

Зміниться і синтаксис програми: додамо варіант

<програма> ::=program <списокоб’явленьфункцій> begin<оператор> end

де <списокоб’явленьфункцій> може бути порожнім, або складатися з об’явленьфункцій перерахованих через кому. Так ми додамо можливість використовувати функції із списку об’явленьфункцій

Синтаксис об’явленняфункції митаме такий вигляд:

<об’явленняфункції>::=func<ім’я функції>=<вираз> |

func<ім’я функції>(<списокформальних параметрів>)= <вираз>

де список формальних параметрів це список змінних перерахованих через кому.

Синтаксис виклику функції має вигляд:

<виклик функції>::=<ім’я функції> , якщо функція не має параметрів, та

<виклик функції> ::=<ім’я функції> (<список фактичних параметрів>) де список фактичних параметрів – список виразів перерахованих через кому.

Семантика суперпозиції при цьому може бути 2-х видів:

Глобальною суперпозицією функцій g1,g2,…,gn в номінативну функцію f називається функція, яка задається формулою: S(v₁,v₂,..v_n)(f,g₁,g₂,…,g_n)(st) = f([v₁®g₁(st),v₂®g₂(st),…,v_n®g_n(st)])

Локальною суперпозицією функцій g₁,g₂,…,g_n в номінативну функцію f називається функція, яка задається формулою

S[v₁,v₂,..v_n](f,g₁,g₂,…,g_n)(st) = f(stÑ[v₁®g₁(st),v₂®g₂(st),…,v_n®g_n(st)])

+ семантика – формально + повно

…

1.5. пункти і т.д. = оформлення: шрифт (14) + абзаци (відступи) + підписи таблиць (стандарт) + відступи у тексті + міжстрокові…

Приклади задач

…

Задача. Обчислення X^Y через виклик рекурсивної функції множення двох чисел, реалізованої через додавання.

program

func mul(a, b)=if b>0 then a+mul(a,b-1) else 0

begin

res:=1;

while (y>0) do

F₁

F₂

begin

F₃

F₄

res:=mul(x,res);

y:=y-1

end

Дерево синтаксичного виводу програми у мові SIPL:

Повернути, оформити !!!

Transpose picture !!!

Семантичний терм:

sem_P(P)=sem_S(F₁)=sem_S(F₂)=AS^res(1) • sem_S(F₃)=AS^res(1) • WH(sem_B(y>0), sem_S(F₄))=AS^res(1) • WH(S²(gr,y=>,0), AS^res(sem_A(mul(x,res)))• AS^y(S²(sub,y=>,1)))=AS^res(1) • WH(S²(gr,y=>,0), AS^res(S^a,b(sem_A(mul),x=>,res=>)• AS^y(S²(sub,y=>,1))).

Знайдемо sem_A(mul):

sem_A(mul)=IF_A(S²(gr, b=>, 0), sem_A(a+mul(a,b-1)), 0)=IF_A(S²(gr, b=>, 0), S²(add, a=>, sem_A(mul(a,b-1)), 0)=IF_A(S²(gr, b=>, 0), S²(add,a=>,S^a,b(sem_A(mul),a=>,S²(sub,b=>,1))), 0)

Маємо рекурсивно задану семантику для функції.

Доведемо, що sem_A(mul)([aaA, baB])=A*B індукцією за B.

1) База. Якщо B=0, то

sem_A(mul)(st)= IF(S²(gr,b=>,0),S²(add,a=>,S^a,b(sem_A(mul),a=>,S²(sub,b=>,1))),0)(st)=0, оскільки B=0.

2) Припущення. Нехай sem_A(mul)([aaA, baB])=A*B, для всіх B<k.

3) Крок індукції. Нехай B=k>0, маємо:

sem_A(mul)(st)=

IF_A(S²(gr,b=>,0),S²(add,a=>,S^a,b(sem_A(mul),a=>,S²(sub,b=>,1))),0)(st)=

S²(add,a=>,S^a,b(sem_A(mul),a=>,S²(sub,b=>,1)))(st). Використовуючи означення локальної композиції, отримаємо:

sem_A(mul)(st)=S²(add,a=>(st),sem_A(mul)(st∇[aaA, baB-1]))=

A+A*(B-1)=A+A*B-A=A*B

Формула доведена.

Доведемо часткову коректність програми.

Нехай на вхід програмі дається стан st=[xaX, yaY]. X,Y≥0

sem_P(P)(st)=AS^res(1) • WH(S²(gr,y=>,0), AS^res(S^a,b(sem_A(mul),x=>,res=>)• AS^y(S²(sub,y=>,1)))(st)=WH(S²(gr,y=>,0), AS^res(S^a,b(sem_A(mul),x=>,res=>)• AS^y(S²(sub,y=>,1)))(st∇[resa1]).

Нехай WH(S²(gr,y=>,0), AS^res(S^a,b(sem_A(mul),x=>,res=>)• AS^y(S²(sub,y=>,1)))=f. Тоді висунемо гіпотезу, що f(st_in)=st_out, де

st_in=[xaU, yaV, resaR] , U,V≥0 – вхідний стан для циклу,

st_out=[xaU, ya0, resaR*U^V]– результат виконання циклу. Доведемо, що ця рівність виконується, індукцією за кількістю ітерацій циклу:

1) База індукції. NumItWH=0. Тому V≤0, з умови V≥0 випливає, що V=0. Тоді рівність f(st_in)=st_out виконується.

2) Припущення. Нехай рівність f(st_in)=st_outвиконується для всіх циклів з кількістю ітерацій менше деякого додатнього k:

NumItWH<k, k>0

3) Крок індукції. Доведемо, що рівність виконується і для циклів з k ітерацій.

f(st_in)=WH(S²(gr,y=>,0),AS^res(S^a,b(sem_A(mul),x=>,res=>)•AS^y(S²(sub,y=>,1)))(st_in). Використаємо формулу: WH(p, f)=IF(p, f •WH(p,f), id), враховуючи, що кількість ітерацій додатня, а тому умова p на початковому стані істина, маємо: (AS^res(S^a^,^b(sem_A(mul),x=>,res=>)•AS^y(S²(sub,y=>,1))•f)(st_in). Розпишемо композицію:

f(st_in)=f(AS^res(S^a,b(sem_A(mul),x=>,res=>)•AS^y(S²(sub,y=>,1)))(st_in))= f(AS^y(S²(sub,y=>,1)(AS^res(S^a,b(sem_A(mul),x=>,res=>)(st_in)))=f(AS^y(S²(sub,y=>,1)([xaU, yaV, resaU*R]))=f([xaU, yaV-1,resaU*R]), оскільки ми виконали одну ітерацію циклу, то для стану [xaU, yaV-1,resaU*R] кількість ітерацій буде k-1, тому, оскільки з умови y>0 випливає, що V-1≥0:

f([xaU, yaV-1,resaU*R])=[xaU, ya0,resa (U*R)*U^(V-1)] - за припущенням індукції. Але [xaU, ya0,resa (U*R)*U^(V-1)]=[xaU, ya0, resaR*U^V]= st_out

Тому f(st_in)=st_out для кожного st_in=[xaU, yaV, resaR], при умові, що U,V≥0. Тому

sem_P(P)=f([xaX, yaY, resa1])=[xaX, ya0, resaX^Y]

Часткова коректність доведена.

Неважко бачити, що значення y на кожній ітерації циклу утворюють строго спадну послідовність, обмежену нулем. В силу скінченності значення y цикл завжди завершить своє виконання, при умові y=0 цикл не буде виконуватись взагалі. В силу скінченності команд програми, вона завжди зупиняється. Тому справджується повна коректність програми.

Завдання для самостійної роботи

Завдання для самостійної роботи:

1. Ділення двох чисел будь-якого знаку.

2. Обчислити: .