2marca2020 prof.drhab.in».AndrzejObuchowicz TeoretycznePodstawyInformatyki

(1)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie

Teoretyczne Podstawy Informatyki

Wykªad 1

wprowadzenie, poprawno±¢ algorytmów

prof. dr hab. in». Andrzej Obuchowicz

Instytut Sterowania i Systemów Informatycznych Uniwersytet Zielonogórski

a.obuchowicz@issi.uz.zgora.pl p. 424 A2

2 marca 2020

(2)

Spis tre±ci

1 Wprowadzenie Warunki zaliczenia Zakres tematyczny Literatura

2 Poprawno±¢ algorytmów Wst¦p

Wªasno±ci algorytmu poprawnego Dowodzenie cz¦±ciowej poprawno±ci poszukiwanie niezmienników Dowodzenie wªasno±ci stopu

Predykat charakterystyczny oraz asercja Najsªabszy warunek wst¦pny

3 Podzi¦kowanie

(3)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Warunki zaliczenia

Warunki zaliczenia

Wykªad: ko«czy si¦ egzaminem pisemnym obejmuj¡cym zagad- nienia omawiane na wykªadzie. Egzamin odbywa si¦ podczas sesji zimowej.

(4)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Zakres tematyczny

Zakres tematyczny Syllabus

(I) Wiadomo±ci wst¦pne: algorytm i jego wªasno±ci, notacja asymptotyczna. Poprawno±¢ algorytmów: algorytm poprawny, poprawno±¢ cz¦±ciowa, wªasno±¢ okre±lono±ci oblicze«, wªasno±¢

stopu; dowodzenie poprawno±ci cz¦±ciowej, dowodzenie wªasno±ci stopu.

(II) Podstawy teorii automatów i j¦zyków: automaty sko«czone i

wyra»enia regularne, gramatyki bezkontekstowe, automaty ze stosem i j¦zyki bezkontekstowe, wªasno±ci j¦zyków bezkontekstowych.

(III) Prymitywne modele algorytmiczne. Teza ChurchaTuringa. Maszyna Turinga i jej warianty. Maszyna o dost¦pie swobodnym. Programy licznikowe.

(IV) Sprawno±¢ algorytmów. Miary efektywno±ci algorytmów. Zªo»ono±¢

przestrzenna i czasowa. Zªo»ono±¢ pesymistyczna i ±rednia. Dolne i

(5)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Zakres tematyczny

Zakres tematyczny

(V) Klasykacja problemów algorytmicznych. Problemy

ªatwo-rozwi¡zywalne i trudno-rozwi¡zywalne. Klasy problemów algorytmicznych: logarytmiczne, wielomianowe, NP, NP-zupeªne i wykªadnicze. Otwarte problemy zwi¡zane z klasykacj¡ problemów algorytmicznych. Dowodzenie NP-zupeªno±ci. Nierozwi¡zywalno±¢ i nierozstrzygalno±¢.

(VI) Algorytmy wspóªbie»ne i probabilistyczne. Staªa i rozszerzaj¡ca si¦

wspóªbie»no±¢. Zªo»ono±¢ iloczynowa. Sieci - wspóªbie»no±¢ o staªych poª¡czeniach. Teza o obliczeniach równolegªych. Klasa Nicka. Algorytmy RNC. Wspóªbie»no±¢ rozproszona.

Bezpiecze«stwo i »ywotno±¢ systemów wspóªbie»nych.

(VII) Algorytmy probabilistyczne niektórych konwencjonalnych problemów algorytmicznych. Probabilistyczne klasy zªo»ono±ci.

(6)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Literatura

Literatura podstawowa

1 Aho A. V., Hopcroft J. E., Ullman J.D.: Algorytmy i struktury danych, Helion, Gliwice, 2003

2 Banachowski L., Kreczmar A.: Elementy analizy algorytmów, WNT, Warszawa, 1982

3 Bilski T., Chmiel K., Stokªosa J.: Zbiór zada« ze zªo»ono±ci obliczeniowej algorytmów, Wydawnictwo Politechniki Pozna«skiej, Pozna«, 1992

4 Cormen T. H., Leiserson C. E., Rivest R. L.: Wprowadzenie do algorytmów, WNT, Warszawa, 1997

5 Harel D.: Rzecz o istocie informatyki, WNT, Warszawa, 2000

6 Hopcroft J. E., Ullmann J.D.: Wprowadzenie do teorii automatów, j¦zyków i oblicze«, PWN, Warszawa, 2003

(7)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Literatura

Literatura uzupeªniaj¡ca

1 Ben Ari M.: Logika matematyczna w informatyce, WNT, Warszawa, 2005

2 Graham R.L., Knuth D.E., Patashnik O.: Matematyka konkretna, PWN, Warszawa, 2002

3 Papadimitriou C. H.: Zªo»ono±¢ obliczeniowa, Helion, Gliwice, 2012

4 Ross K. A., Wright C. R. B.: Matematyka dyskretna, PWN, Warszawa, 2000

5 Wróblewski P.: Algorytmy, struktury danych i j¦zyki programowania, Helion, Gliwice, 1997

(8)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Wst¦p

Problem algorytmiczny

Opis wszystkich poprawnych

danych wejœciowych

Opis

oczekiwanych

wyników jako

funkcji danych

wejœciowych

(9)

Przykªady formuªowania problemów

problem sortowania:

Dane: tablica a₁, a₂, . . . , an)o n elementach typu porz¡dkowego;

Szukane: tablica o tych samych elementach ale uporz¡dkowana niemalej¡co.

problem komiwoja»era:

Dane: nmiast, odlegªo±ci pomi¦dzy ka»d¡ par¡ miast (dij| i, j = 1, 2, . . . , n);

Szukane: trasa komiwoja»era przez wszystkie miasta (ale tylko jedna wizyta w ka»dym mie±cie permutacja miast) o najmniejszej sumie odlegªo±ci.

(10)

Algorytm

Dowolne poprawne dane wejœciowe

Oczekiwane wyniki

Algorytm - rozwi¹zanie problemu algorytmicznego

(11)

Wªasno±ci algorytmu

ALGORYTM KA¯DY KROK

JEDNOZNACZNIE I PRECYZYJNIE ZDEFINIOWANY

KA¯DY MO¯LIWY PRZYPADEK PRZEWIDZIANY

R^OZWI¥ZANIE ZAWSZE OSI¥GNIÊTE I TO W SKOÑCZONEJ LICZBIE KROKÓW

MO¯E KORZYSTAÆ Z DANYCH WEJŒCIOWYCH

PROWADZI DO JEDNEGO LUB WIÊCEJ DANYCH

WYJŒCIOWYCH

WSKAZANA W£ASNOŒÆ OGÓLNOŒCI OPERACJE

PODSTAWOWE

(12)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Wªasno±ci algorytmu poprawnego

Denicja poprawno±ci algorytmicznej

Dowolne poprawne dane wejœciowe

Oczekiwane wyniki Algorytm

a

b

Algorytm nazywamy poprawnym, je»eli dla dowolnych

poprawnych danych wej±ciowych (speªniaj¡cych warunek α) algorytm osi¡ga punkt ko«cowy i otrzymujemy poprawne wyniki (speªniaj¡cych warunek β).

(13)

Cechy algorytmu poprawnego

Algorytm poprawny

Czêœciowa

poprawnoœæ W³asnoœæ

stopu W³asnoœæ

okreœlonoœci obliczeñ

+ +

(14)

Cz¦±ciowa poprawno±¢

Algorytm poprawny

Czêœciowa

stopu W³asnoœæ

+ +

Algorytm nazywamy cz¦±ciowo poprawnym, gdy prawdziwa jest nast¦puj¡ca implikacja: je»eli dla dowolnych poprawnych danych wej-

±ciowych algorytm osi¡gnie koniec, to dane wyj±ciowe b¦d¡ speªnia¢

warunek ko«cowy.

(15)

Wªasno±¢ okre±lono±ci oblicze«

Algorytm poprawny

Czêœciowa

stopu W³asnoœæ

+ +

Algorytm posiada wªasno±¢ okre±lono±ci oblicze«, je»eli dla dowolnych poprawnych danych wej±ciowych dziaªanie algorytmu nie zostanie przerwane.

(16)

Wªasno±¢ stopu

Algorytm poprawny

Czêœciowa

stopu W³asnoœæ

+ +

Algorytm posiada wªasno±¢ stopu, je»eli dla dowolnych poprawnych danych wej±ciowych algorytm nie b¦dzie dziaªaª w niesko«czono±¢.

(17)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Dowodzenie cz¦±ciowej poprawno±ci

Metoda niezmienników Floyda

metoda post¦powania:

wyró»ni¢ newralgiczne punkty w algorytmie;

okre±li¢ warunki (niezmienniki), jakie maj¡ by¢

speªnione w ka»dym wyró»nionym punkcie;

udowodni¢ poprawno±¢ kolejnych warunków zakªadaj¡c poprawno±¢ warunków poprzedzaj¡cych.

(18)

Metoda niezmienników Floyda - punkty newralgiczne

Instrukcja B W

Instrukcja A

T W N T N

Instrukcja A

struktury steruj¡ce:

bezpo±rednie nast¦pstwo;

wybór warunkowy;

iteracja ograniczona;

iteracja warunkowa (nieograniczona);

(19)

Metoda niezmienników Floyda - punkty newralgiczne, cd

Instrukcja A

k=inc(k) T

N k=kmin

k>kmax

wybór warunkowy;

(20)

Metoda niezmienników Floyda - punkty newralgiczne, cd

Instrukcja A T

N W

Instrukcja A

T

N W

wybór warunkowy;

(21)

Metoda Floyda przykªad

T N

STOP

x,y

r>=y q=q+1

r=r-y

q=0 r=x

START

q,r

1

2

3

1. α : x ≥ 0 ∧ y ≥ 0

2. γ : x = q ∗ y + r ∧ r ≥ 0 ∧ y ≥ 0 3. β : x = q ∗ y + r ∧ 0 ≤ r < y 2 2.

γ⁰: x = q⁰∗ y + r⁰∧ r⁰≥ 0 ∧ y⁰≥ 0 x = (q +1) ∗ y + r − y =

= q∗ y + y + r − y = q ∗ y + r r⁰≥ 0 ⇒ r − y ≥ 0 ⇒ r ≥ y

(22)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie poszukiwanie niezmienników

Suma ci¡gu elementów 1/5

Problem opracowa¢ algorytm do obliczenia sumy elementów nale»¡cych do pewnej sekwencji A:

Krok 1: a = [ai|i = 1, 2, . . . n]

Krok 2: S =Pn i =1ai

Krok 3: S :=0; for i := 1 to n do S = S + a[i];

Etapy poszukiwania warunków:

A) opracowa¢ schemat blokowy,

B) okre±li¢ warunki, po realizacji poszczególnych instrukcji.

(23)

Suma ci¡gu elementów 2/5

START

i ← 1

S ← 0

i > n TAK

NIE

S ← S+ ai

STOP

i ← i+ 1

(24)

Suma ci¡gu elementów 3/5

START

i ← 1

S ← 0

i > n TAK

NIE

S ← S+ ai

STOP

i ← i+ 1 n ∈N

n ∈N ∧ i = 1

n ∈N ∧ i = 1 ∧ S = 0

(25)

Suma ci¡gu elementów 4/5

START

i ← 1

S ← 0

i > n TAK NIE

S ← S+ ai

STOP

i ← i+ 1 n ∈ N

n ∈ N ∧ i= 1

n ∈ N ∧ i= 1 ∧ S = 0

n ∈ N ∧ i ∈ N ∧ i ≤ n+ 1 ∧ S =i−1 j=1aj

n ∈ N ∧ i ∈ N ∧ i= n + 1 ∧ S =i−1 j=1aj; S =n

j=1aj

n ∈ N ∧ i ∈ N ∧ i ≤ n ∧ S=i−1 j=1aj

n ∈ N ∧ i ∈ N ∧ i ≤ n ∧ S=i j=1aj

n ∈ N ∧ i ∈ N ∧2 ≤ i ≤ n + 1 ∧ S =i−1 j=1aj

(26)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Dowodzenie wªasno±ci stopu

Dowodzenie wªasno±ci stopu metoda liczników iteracji

begin

p := c; while ι do begin

K; p := p +1 end end

deniujemy ograniczenie τ i dowodzimy, »e przed ka»d¡ werykacj¡

warunku ι speªniony jest niezmiennik p ≤ τ

(27)

Metoda liczników iteracji przykªad

T N

STOP

x,y

r>=y q=q+1

r=r-y

q=0 r=x

START

q,r

1

2

3

1. α : x ≥ 0 ∧ y > 0

2. γ : x = q ∗ y + r ∧ r ≥ 0 ∧ y > 0 δ : q≤ τ = ^xy

3. β : x = q ∗ y + r ∧ 0 ≤ r < y δ : x = q∗ y + r ⇒ ^xy = q +_y^r ⇒

⇒ q = ^xy −y^r ≤ ^xy

(28)

Dowodzenie wªasno±ci stopu metoda malej¡cych wielko±ci

begin

while ι do begin

K (3 w := w − c) end end

istnieje wyra»enie w ≥ 0, które zmniejsza sw¡ warto±¢

w ka»dej iteracji, ale jest ograniczone od doªu przez 0.

(29)

Metoda malej¡cych warto±ci przykªad

T N

STOP

x,y

r>=y q=q+1

r=r-y

q=0 r=x

START

q,r

1

2

3

1. α : x ≥ 0 ∧ y > 0

2. γ : x = q ∗ y + r ∧ r ≥ 0 ∧ y ≥ 0 3. β : x = q ∗ y + r ∧ 0 ≤ r < y 2 2. r ≥ y ⇒ r − y ≥ 0 ⇒ r⁰ ≥ 0

(30)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Predykat charakterystyczny oraz asercja

Predykat charakterystyczny i stan programu

Denicja stanu programu za [Ben Ari, 2005]:

Stan programu

Je±li w programie wyst¦puje n zmiennych (x₁, x₂, . . . , xn), to stan s okre±la krotka (v(x₁), v (x₂), . . . , v (xn)), gdzie v(xi)jest warto±ci¡

zmiennej xi.

Predykat charakterystyczny

Niech U b¦dzie zbiorem wszystkich krotek utworzonych z elementów pewnej dziedziny (lub dziedzin). Niech U⁰ ⊆ U. Predykat charakterystyczny PU⁰(v (x₁), . . . , v (xn))zbioru U⁰ jest zdeniowany tak, aby

U⁰={(v(x1), . . . , v (x_n))∈ U|P^U⁰(v (x₁), . . . , v (x_n)]}.

(31)

Predykat charakterystyczny

Niech U = C × C, a U⁰ ⊆ U niech b¦dzie nast¦puj¡cym zbiorem par liczb:

... (-2, -1) (-2, 0) (-2, 1) (-2, 2) (-2, 3)...

... (-1, -1) (-1, 0) (-1, 1) (-1, 2) (-1, 3) ... (0, -1) (0, 0) (0, 1) (0, 2) (0, 3) ... (1, -1) (1, 0) (1, 1) (1, 2) (1, 3) ... (2, -1) (2, 0) (2, 1) (2, 2) (2, 3)

...

Predykatem charakterystycznym zbioru U⁰ jest (x1= x₁)∧ (x2≤ 3) lub po uproszczeniux₂≤ 3.

Program posiadaj¡cy dwie zmienne caªkowite mo»e rozpocz¡¢ wykonywanie w jednym z 2³²· 2³² ≈ 10¹⁹ stanów na 32-bitowym kom- puterze! Dlatego, zamiast wnioskowania o stanach, konieczne jest

(32)

Predykat charakterystyczny

Przykªad zwi¡zany z poj¦ciem predykatu charakterystycznego:

Niech S b¦dzie instrukcj¡ programu o postaci x := 2 ∗ y + 1, która przeksztaªca stan {(x, y)|true} w stan {(x, y)|x := 2y + 1}.

Zakªada si¦, »e zbiorem stanów pocz¡tkowych jest {(x, y)|y ≤ 3}.

Poniewa» (y ≤ 3) ⇒ (2y + 1 ≤ 7), wiec stan ko«cowy po wykonaniu instrukcji S b¦dzie elementem zbioru {(x, y)|(x ≤ 7) ∧ (y ≤ 3)}.

Mówi si¦, »e S przeksztaªca stan y ≤ 3 w (x ≤ 7) ∧ (y ≤ 3).

(33)

Asercja

Denicja asercji {p} code {q}

Asercj¡ nazywamy trójk¦ {p} code {q}, gdzie code jest programem na- tomiast p i q, s¡ formuªami rachunku predykatów, nazywanewarunkiem wst¦pnymorazwarunkiem ko«cowym.

Asercja jest prawdziwa, co oznaczamy |= {p} code {q}, wtedy i tylko wtedy. gdy zachodzi warunek: je±li program code rozpocznie wykonywanie w stanie speªnia- j¡cym p oraz obliczenie code zako«czy si¦, to obliczenie zako«czy si¦ w stanie speªniaj¡cym q. Je±li |= {p} code {q}, to program S jest cz¦±ciowo poprawny wzgl¦dem p i q.

Przykªad asercji:

|= {y ≤ 3} x := 2 · y + 1 {x ≤ 7 ∧ y ≤ 3}

Asercje trywialne

Dla ka»dego programu S oraz dowolnego q zachodzi |= {false}S{q}, gdy» nie

(34)

Warunek, wa»na rzecz

Co wiadomo o takiej asercji: |= {y ≤ 3} x := 2 · y + 1 {x ≤ 7 ∧ y ≤ 3}

Warunek y ≤ 3 nie jest jedynym warunkiem wst¦pnym zapewniaj¡cym speªnienie warunku ko«cowego.

Innym warunkiem wst¦pnym jest np.: y = 1 ∨ y = 3.

Warunek y = 1 ∨ y = 3 jest bardziej szczegóªowy ni» y ≤ 3 gdy» nie opisuje wszystkich stanów, z których obliczenie mo»e przej±¢ do stanu speªniaj¡cego warunek ko«cowy.

Nale»y wybiera¢ najmniej ograniczaj¡cy warunek pocz¡tkowy, tak aby stanem pocz¡tkowym okre±lonego obliczenia mogªa by¢ jak najwi¦ksza liczba stanów.

(35)

Wprowadzenie Poprawno±¢ algorytmów Podzi¦kowanie Najsªabszy warunek wst¦pny

Najsªabszy warunek wst¦pny NWW

Denicja okre±la najsªabsz¡ formuª¦ w rozpatrywanym w danym momencie zbiorze formuª:

Formuªa A jest sªabsza od formuªy B, je±li B → A. Dla danego zbioru formuª {A1, A₂, . . .} formuªa Aⁱ, jest najsªabsz¡ formuª¡ tego zbioru, je±li Aj → Aⁱ dla ka»dego j.

Najsªabszy warunek wst¦pny jest bardzo przydatny w procesie okre±lenia asercji dla instrukcji b¡d¹ zbioru instrukcji S.

Niech b¦dzie dany program S oraz formuªa q, najsªabszym warunkiem wst¦pnym S oraz q nazwiemy tak¡ formuª¦ p dla której zachodzi |=

{p}S{q}, co oznaczymy jako NWW(S, q).

O czym mówi równie» poni»szy lemat:

(36)

Najsªabszy warunek wst¦pny ilustracja

Formuªa y ≤ 3 jest sªabsza od formuªy y = 1 ∨ y = 3, która z kolei jest sªabsza od formuªy y = 1, tak wiec y ≤ 3 jest sªabsza od y = 1.

y≤ 3

y = 0 y = 1 y = 2 y = 3

y = 1∨ y = 3

Inne uwagi o predykatach w NWW:

zawsze mo»na wzmocni¢ poprzednik i osªabi¢ nast¦pnik implikacji.

Je±li p ⇒ q, to równie» (p ∧ r) ⇒ q oraz p ⇒ (q ∨ r).

(37)

Najsªabszy warunek wst¦pny inne konstrukcje

Poj¦cie najsªabszego warunku wst¦pnego mo»e by¢ zastosowane do wyzna- czania niezmienników albo warunków wst¦pnych. Poj¦cie to mo»e by¢ sto- sowane do podstawowych instrukcji jak przypisanie, p¦tla while, instrukcja warunkowa.

Przypisanie

NWW(x := t, p(x)) = p(x){x ← t}

Sekwencja instrukcji

NWW(S₁; S₂, q) = NWW (S₁, NWW (S₂, q))

Istnieje mo»liwo±¢ wykorzystania NWW do denicji niezmiennika:

Warunek N nazwiemy niezmiennikiem wtedy i tylko wtedy, gdy NWW(S, N ) = N .

(38)

Najsªabszy warunek wst¦pny inne konstrukcje

NWW dla instrukcji warunkowej oraz p¦tli typu dopóki:

O instrukcji warunkowej

NWW(if W then S1else S2, q) = (W →NWW(S1, q)) ∧ (¬W →NWW(S2, q))

albo

NWW(if W then S1else S2, q) = (W ∧NWW(S1, q)) ∨ (¬W ∧NWW(S2, q))

O p¦tli dopóki

NWW(while W do S, q) = (¬W → q) ∧ (W → NWW(S; while W do S, q))

albo

(39)

NWW przykªady

Przykªady NWW:

1 NWW(x := 2 ∗ y + 1; x ≤ 7 ∧ y ≤ 3) = y ≤ 3,

2 NWW(x := 2 ∗ y + 1; x ≤ 7) = y ≤ 3,

3 NWW(x := 2 ∗ y + 1; x ≤ 9) = y ≤ 4,

4 NWW(x := y + 2; x ≤ 7) = y ≤ 5,

5 NWW(y := y − 1; y ≥ 0) = y − 1 ≥ 0 ≡ y ≥ 1.

NWW dla dwóch instrukcji przypisania:

NWW(x := x + 1; y := y + 1; x < y)

=NWW(x := x + 1; NWW(y := y + 1; x < y))

=NWW(x := x + 1; x < y + 1)

=x +1 < y + 1 ≡ x < y

(40)

NWW przykªady

Czego dotyczy poni»szy przykªad:

NWW(x := x + a; y := y − 1; x = (b − y) · a)

=NWW(x := x + a; NWW(y := y − 1; x = (b − y) · a))

=NWW(x := x + a; x = (b − y + 1) · a)

=x + a = (b− y + 1) · a ≡x = (b− y) · a Drugi przykªad:

NWW(x := x + 1; y ≥ 0) =y ≥ 0 Instrukcja warunkowa:

NWW(if y = 0 then x := 0 else x := y + 1; x = y)

=(y =0 ⇒ NWW(x := 0; x = y)) ∧ (y 6= 0 ⇒ NWW(x := y + 1; x = y))

=(y =0 ⇒ y = 0) ∧ (y 6= 0 ⇒ y + 1 = y)

(41)

NWW przykªady

NWW dla przykªadowej p¦tli while, gdzie W oznacza while x > 0 do x := x − 1:

NWW(W ; x = 0)

=(¬(x > 0) ∧ (x = 0)) ∨ ((x > 0) ∧ NWW(x := x − 1; W ; x = 0))

≡(x = 0) ∨ ((x > 0) ∧ NWW(x := x − 1; NWW(W ; x = 0)))

≡(x = 0) ∨ ((x > 0) ∧ NWW(W ; x = 0){x ← x − 1})

≡(x = 0) ∨ ((x > 0) ∧ [(x − 1 = 0) ∨ ((x − 1 > 0)∧

NWW(W ; x = 0){x ← x − 1}{x ← x − 1])

≡(x = 0) ∨ (x = 1) ∨ (x > 1 ∧ NWW(W ; x = 0){x ← x − 1}{x ← x − 1}) Ko«cowa posta¢:

NWW(W ; x = 0)

≡(x = 0) ∨ (x = 1) ∨ (x = 2) ∨ . . .

(42)

Wa»ne wªasno±ci NWW

Twierdzenie o rozdzielaniu NWW:

|= NWW(S, p) ∧ NWW(S, q) ⇔ NWW(S, p ∧ q) Wniosek, logika jednak dziaªa albo cudu nie ma:

|= NWW(S, p) ∧ NWW(S, ¬p) ⇔ NWW(S, false) Dualizm NWW:

|= ¬NWW(S, ¬p) ⇒ NWW(S, p) Monotoniczno±¢:

(p⇒ q) ⇒ (|= NWW(S, p) ⇒ NWW(S, q))

(43)

2marca2020 prof.drhab.in».AndrzejObuchowicz TeoretycznePodstawyInformatyki

Teoretyczne Podstawy Informatyki

Spis tre±ci

Warunki zaliczenia

Zakres tematyczny  Syllabus

Zakres tematyczny

Literatura podstawowa

Literatura uzupeªniaj¡ca

Problem algorytmiczny

Opis wszystkich poprawnych

danych wejœciowych

Opis

oczekiwanych

wyników jako

funkcji danych

wejœciowych

Przykªady formuªowania problemów

Algorytm

Wªasno±ci algorytmu

Denicja poprawno±ci algorytmicznej

Cechy algorytmu poprawnego

+ +

Cz¦±ciowa poprawno±¢

+ +

Wªasno±¢ okre±lono±ci oblicze«

+ +

Wªasno±¢ stopu

+ +

Metoda niezmienników Floyda

Metoda niezmienników Floyda - punkty newralgiczne

Metoda niezmienników Floyda - punkty newralgiczne, cd

Metoda niezmienników Floyda - punkty newralgiczne, cd

Metoda Floyda  przykªad

Suma ci¡gu elementów 1/5

Suma ci¡gu elementów 2/5

Suma ci¡gu elementów 3/5

Suma ci¡gu elementów 4/5

Dowodzenie wªasno±ci stopu  metoda liczników iteracji

Metoda liczników iteracji  przykªad

Dowodzenie wªasno±ci stopu  metoda malej¡cych wielko±ci

Metoda malej¡cych warto±ci  przykªad

Predykat charakterystyczny i stan programu

Predykat charakterystyczny

Predykat charakterystyczny

Asercja

Warunek, wa»na rzecz

Najsªabszy warunek wst¦pny  NWW

Najsªabszy warunek wst¦pny  ilustracja

Najsªabszy warunek wst¦pny  inne konstrukcje

Najsªabszy warunek wst¦pny  inne konstrukcje

NWW  przykªady

NWW  przykªady

NWW  przykªady

Wa»ne wªasno±ci NWW

Dzi¦kuj¦ za uwag¦!!!

Zakres tematyczny Syllabus

Denicja poprawno±ci algorytmicznej

Metoda Floyda przykªad

Dowodzenie wªasno±ci stopu metoda liczników iteracji

Metoda liczników iteracji przykªad

Dowodzenie wªasno±ci stopu metoda malej¡cych wielko±ci

Metoda malej¡cych warto±ci przykªad

Najsªabszy warunek wst¦pny NWW

Najsªabszy warunek wst¦pny ilustracja

Najsªabszy warunek wst¦pny inne konstrukcje

Najsªabszy warunek wst¦pny inne konstrukcje

NWW przykªady

NWW przykªady

NWW przykªady