Principy programovacích jazyku˚ PB006
PB006
1
Náplnˇ kursu Pˇrehled programovacích paradigmat, vlastností programovacích jazyku˚ a zkoumání teoretické podstaty jevu, ˚ které se v programovacích jazycích vyskytují.
Pˇrednáška Podzim 2009: úterý 18:00–19:40 D3
Konsultace ˇ 18:00–19:00 v B419 Konsultaˇcní hodiny (do 17. 12.): pondelí
Aktuální informace
http://www.fi.muni. z/~libor/vyuka/PB006/ PB006
2
Literatura - R. D. Tennent: Principles of Programming Languages, Prentice Hall, 1981 - D. A. Watt: Programming Languages Concepts and Paradigms, Prentice Hall, 1990 - T. W. Pratt, M. V. Zelkowitz: Programming Languages – Design and Implementation, Prentice Hall, 1996
PB006
3
Úvod Historie programovacích jazyku˚ Paradigmata Klasifikace jazyku˚
PB006
4
TM
PL
λ
Assembler 1950 Lisp Fortran Cobol
1960
Algol60 Snobol
Basic 1970
PL/1
Algol68
Forth Simula
Prolog
Pascal
Smalltalk 1980
C
Modula
PostScript
ML
Ada Eiffel
Occam
Scheme
C++ Hope
Oberon Erlang
1990 Java
Clean
Miranda
Tcl
Gödel Perl
Python
Php
2000
Haskell
Cayenne
Ruby
PB006
5
Klasifikace programovacích jazyku˚ Paradigma - imperativní / funkcionální / logické / CLP - procedurální / objektoveˇ orientované - deterministické / nedeterministické - sekvenˇcní / paralelní
Struktura programu - amorfní / blokové / modulární / objektové
PB006
6
Typový systém - netypované / typované - odvozování typu: ˚ statické / dynamické - typy: * monomorfní / polymorfní * parametrický / inklusní / ad hoc polymorfismus podtypy, pˇretížení, druhy, PTS
PB006
7
Vztah k výpoˇctu - kompilované / interpretované - dávkové / interaktivní / knihovní
Oblast nasazení - cˇ íselné výpoˇcty / zpracování textu˚ / syst. programování / simulace / AI / GUI / VR
Doba vzniku Rozšíˇrení ...
PB006
8
Aspekty programovacího jazyka Pragmatika - použitelnost jazyka - oblast nasazení - snadnost implementace - vztah k výpoˇctu ˇ - úspešnost jazyka
PB006
9
Syntax - struktura a forma jazyka - je popsána formální gramatikou, cˇ asto ve dvou až tˇrech úrovních (lexikální, bezkontextová, kontext. omezení) - konkrétní / abstraktní syntax
Sémantika - význam - vztah mezi programem a výpoˇcetním modelem - denotaˇcní / operaˇcní sémantika - axiomatická sémantika PB006
10
Syntax Konkrétní a abstraktní syntax Lexikální a frázová syntax Typová a kontexová omezení
PB006
11
Konkrétní syntax Popsána formální gramatikou G
= (N; ; P; S ),
N; ; P koneˇcné, N \ = ;, S 2 N , P ((N [ ) N (N [ ) ) (N [ ) , v pˇrípadeˇ programovacích jazyku˚ tato gramatika bývá bezkontextová, tj.
P
PB006
N (N [ ) [ f(S; ")g. +
12
Pro zápis bezkontextových gramatik existují ruzné ˚ formalismy
G=
fIdent; Písmenog; f’a’; ’b’; ’_’g;
f(Ident; Písmeno); (Ident; Ident Písmeno ); (Ident; Ident _ Písmeno); (Písmeno; ’a’); (Písmeno; ’b’)g; Ident
BNF Ident Písmeno
::= ::=
EBNF Ident Písmeno
PB006
Písmeno
a
jb
::= ::=
j Ident Písmeno j Ident _ Písmeno (
Písmeno Písmeno
a
jb
j _ Písmeno)
13
Syntaktický diagram:
Ident
Písmeno _
a Písmeno b
PB006
14
Syntax programovacího jazyka bývá obvykle popsána ve více úrovních.
Lexikální syntax – mikrosyntax Popisuje lexikální strukturu jazyka. Slouží k vymezení lexika – množiny lexikálních atomu˚ neboli lexému. ˚ Bývá popsána regulární gramatikou nebo jednoduchou bezkontextovou gramatikou. Terminály gramatiky jsou znaky. Vlastní program je pak definován jen jako posloupnost lexikálních atomu. ˚ Mikrosyntax lze pˇrirovnat k morfologii v pˇrirozeném jazyce – tvoˇrí jeho slovník ("o ).
Kromeˇ toho, že lexikální syntax vymezuje lexikální atomy, popisuje i místo, které je ˇ oddeluje: tzv. bílé místo a komentáˇre. Proto zejména v jazycích se zanoˇrovanými komentáˇri nestaˇcí pro popis mikrosyntaxe regulární gramatika.
PB006
15
Frázová syntax – makrosyntax Popisuje úplnou strukturu programu. Bývá popsána bezkontextovou gramatikou. Terminály gramatiky jsou lexikální atomy. ˇ Makrosyntax lze pˇrirovnat k vetné skladbeˇ (
& ) pˇrirozeného jazyka – tvoˇrí množinu
ˇ správneˇ vytvoˇrených vet.
Kontextová omezení Podmínky vymezující podmnožinu jazyka generovaného gramatikou frázové syntaxe. Obvykle zaruˇcují, že v programu použité symboly jsou definovány/deklarovány, operátory mají správné arity, program je otypovatelný. Kontextovým omezením se také ˇríká statická sémantika. Analogií kontextových omezení v pˇrirozeném jazyce jsou pravidla vyluˇcující (jinak syntakticky ˇ jako „Zelené myšlenky zuˇriveˇ spí.“ správné, ale nesmyslné) vety PB006
16
Makrojazyk ˇ ˇ druhým jazykem M – tzv. makrojazykem, Casto bývá programovací jazyk L doplnen
který pˇredzpracovává program v jazyce L.
Zdrojové texty programu˚ dávané kompilátoru (nebo interpretu) jsou programy ˇ (u makrojazyku˚ se ˇríká expandují) ješteˇ v makrojazyce M . Tyto programy se provádejí v dobeˇ pˇrekladu, typicky hned po analýze lexikální syntaxe. Výsledek expanze je program v jazyce L, který jde na vstup analyzátoru frázové syntaxe. ˇ vyjádˇrit napˇr. podmínený ˇ pˇreklad nebo cpp makrojazyk pro C; primitivní, ale lze v nem vkládání textu z jiných souboru˚ Scheme v programech lze použít makrojazyk, který má tutéž syntax a stejné funkce jako Scheme ˇ anebo ve spojení s nejakým ˇ M4 univerzální makrojazyk, použitelný bud’ samostatne, PB006
programovacím jazykem jako jeho pˇredzpracující makrojazyk
17
Konkrétní a abstraktní syntax Konkrétní syntax - definuje vlastní jazyk ˇ - obsahuje dostateˇcneˇ mnoho terminálu, ˚ které zjednodušují a zjednoznaˇcnují syntaktickou analýzu i cˇ itelnost programu
Abstraktní syntax - popisuje strukturu - obsahuje pˇredevším neterminály - terminály slouží pouze jako diskriminátory odvozovacích pravidel - vhodná pro formální práci s jazykovými termy, napˇr. pro definici denotaˇcní sémantiky
PB006
18
Pˇríklad – abstraktní syntax výrazu˚
E ::= L j V
j E or E j E and E j E = E j E < E j E + E j E E
Chápána jako konkrétní syntax je gramatika nejednoznaˇcná, od této nejednoznaˇcnosti ˇ u˚ pracujeme pˇrímo s termy, jež svou strukturou však abstrahujeme tím, že místo ˇretezc vyjadˇrují i odvození pˇríslušného slova
PB006
19
x + 2 +
y = 8
+
x
*
x
* 2
=
= y
8
* 2
8
x
PB006
2 y
8
= 8
y
+ y
8
*
* 2
x
=
y
= +
+
x
2
20
S ::= P j : : : P ::= if E then S E ::= : : :
PB006
j if E then S else S
21
0
if then if then p else q
if
S
S
P
P
E
then
c
S
E c’
E
then
c
P if
PB006
if
then
S p
else
S q
S
S
else
q
P if
E c’
then
S p
22
Abstraktní syntax Pravidla (bezkontextové) konkrétní syntaxe
A ::= 1;0 B1;1 1;1 : : : 1;r1 1 B1;r1 1;r1 j 2;0B2;1 2;1 : : : 2;r2 1 B2;r2 2;r2 j m;0Bm;1 m;1 : : : m;rm 1 Bm;rm m;rm odpovídají disjunktnímu sjednocení
A^ = (B^1;1 B^1;r1 ) [_ (B^2;1 B^2;r2 ) [_ [_ (B^m;1 B^m;rm ) PB006
23
Protože sjednocení je disjunktní, má každý jeho cˇ len jako pˇríznak celé pˇríslušné pravidlo ˇ ˇ gramatiky (v praxi však vetšinou zkrácené na nejaký význaˇcný terminál, který toto pravidlo jednoznaˇcneˇ urˇcuje).
^
Prvky sjednocení S odpovídají slovum ˚ jazyka, ale i s jejich derivací Proto je abstraktní syntax vždy jednoznaˇcná. Ale je cˇ asto zavedena gramatikou, kterou když cˇ teme jako gramatiku konkrétní syntaxe, je tato konkrétní gramatika je nejednoznaˇcná. V bezkontextových jazycích se však tato ˇ jazyka a lze ji obejít napˇríklad vhodným nejednoznaˇcnost týká pouze struktury vet uzávorkováním.
PB006
24
Typy
PB006
25
Základní (primitivní, atomické) skalární
logické hodnoty znaky (krátké, dlouhé) cˇ ísla (celá, desetinná, . . . ) adresy .. .
Složené
kartézský souˇcin disjunktní sjednocení zobrazení (pole, funkce) PB006
souˇcinové souˇctové mocninné 26
Kartézský souˇcin
AB Množina všech uspoˇrádaných dvojic Funkcím
(a; b) takových, že a : A, b : B .
:AB !A fst (x; y ) = x snd : A B ! B snd (x; y ) = y
fst
ˇríkáme projekˇcní funkce nebo selektory. Je-li z
= (x; y) : A B ,
ABC
pak x
= fst z; y = snd z.
Podobneˇ pro kartézský souˇcin tˇrí a více typu. ˚ PB006
27
Agregáty V typu agregátu jsou definovány projekˇcní funkce, cˇ asto se zvláštní postfixovou syntaxí. Je-li Datum
= fden : Int; mesic : String; rok : Intg
d : Datum d = fden = 5; mesic = "°íjen"; rok = 2005g pak zápis d:den = 5 odpovídá den (d) = 5.
PB006
28
ˇ Casto syntax jazyka vyžaduje, aby bylo jednoznaˇcneˇ ˇreˇceno, kterého typu agregátu je daná hodnota:
d = Datumfden = 5; mesic = "°íjen"; rok = 2005g
PB006
29
Disjunktní sjednocení
A+B
( )
(
)
Sjednocení množiny všech dvojic L; a s množinou všech dvojic R; b , kde a
b : B.
L, R jsou pˇríznaky puvodu ˚ prvku a, resp. b.
Funkcím
: A,
:A!A+B inl x = (L; x) inr : B ! A + B inr y = (R; y ) inl
ˇríkáme inserˇcní funkce nebo konstruktory. Je-li x
: A, y : B , u = (L; x), v = (R; y), pak u = inl x, v = inr y.
A+B+C
Podobneˇ pro disjunktní sjednocení tˇrí a více typu. ˚ PB006
30
Uniony V typu unionu jsou definovány inverze konstruktoru, ˚ cˇ asto se zvláštní postfixovou syntaxí. Je-li Cislo
pak zápis
:cele = 42
= fcele : Int j desetinne : Floatg
: Cislo
= fcele = 42g odpovídá inl
42 = .
ˇ Nekdy se vyžaduje, aby bylo jednoznaˇcneˇ ˇreˇceno, kterého typu unionu je daná hodnota:
= Cislo fcele = 42g
PB006
31
Obecné vlastnosti kartézského souˇcinu a disjunktního sjednocení
f : C ! A, g : C ! B Pak existuje jediná funkce h : C ! A B tak, že Necht’ A, B , C jsou typy,
ˇ nejaké dveˇ funkce.
= f snd Æ h = g fst Æ h
fst
A
f
AxB
snd
h
g
B
C PB006
32
Necht’ A, B , C jsou typu, Pak existuje jediná funkce
f : A ! C, g : B ! C h : A + B ! C tak, že
ˇ nejaké dveˇ funkce.
h Æ inl = f h Æ inr = g inl
A
f
A+B
h
inr
B
g
C PB006
33
Pole Zobrazení (koneˇcného) ordinálního typu I do typu T .
(Koneˇcný typ I je ordinální Zápis:
PB006
Array I
, existuje bijekce ord : I ! f1; : : : ; ng, kde n = jI j.)
T
34
ˇ Vícerozmerná pole
p=
q=
I
I
z
{
11 12 13 14 21 22 23 24
8 > z > > > < 11 > z > > > :
J
}|
J
}| }|
(I J ) T
{
12 13 14 J
Array
{
(
Array I Array J
T)
21 22 23 24
p[i; j ℄ = q[i℄[j ℄ PB006
35
Funkce Zobrazení typu A do typu B . Zápis: A
!B
ˇ ˇ arity) Funkce více promenných (vetší
0
f=
0
g=
(1; 1) 7! 11 (1; 2) 7! 12 (1; 3) 7! 13 (1; 4) 7! 14 (2; 1) 7! 21 (2; 2) 7! 22 (2; 3) 7! 23 (2; 4) 7! 24 1
1 7! 1 7! 11 2 7! 12 3 7! 13 4 7! 14 2 7! 1 ! 7 21 2 ! 7 22 3 ! 7 23 4 ! 7 24
A
1 A
AB ! C
A ! (B ! C )
f (x; y) =gxy PB006
36
Potenˇcní množiny Mocninný typ, speciální pˇrípad zobrazení. Set A
A ! Bool
typ všech podmnožin A typ všech predikátu˚ nad A
: Set A odpovídá tzv. charakteristická funkce : A ! Bool taková, že pro každé x : A platí x 2 a , (x) = true. Každé hodnoteˇ a
a
a
PB006
37
Výˇctové typy Zvláštní pˇrípad disjunktního sjednocení, kdy všechny inserce jsou typu Unit
! T.
= ffalse : Unit j true : Unitg Tyden = fpo : Unit j út : Unit j : : : j ne : Unitg ffalse = ()g; ftrue = ()g; fpo = ()g; : : : Bool
zkracujeme na
= false j true Tyden = po j út j st j cˇ t j pá j so j ne Bool
false; true ; po ; : : :
PB006
38
Prázdný typ Void
(disjunktní sjednocení nulového poˇctu typu) ˚
Neobsahuje žádnou hodnotu.
Jednotkový typ Unit Má jedinou hodnotu – uspoˇrádanou nultici
PB006
(kartézský souˇcin nulového poˇctu typu) ˚
().
39
Rekursivní (induktivní) typy Je-li F
ˇ (t) zápis typu˚ („typový výraz“) obsahující typovou promennou t, pak
FIX t: F (t) ˇ nejmenší typ vyhovující rovnici je (množinove)
t = F (t) Definici typu T
ˇ = FIX t: F (t) zapisujeme struˇcneji
T = F (T ) a mluvíme o tzv. rekursivní definici typu.
PB006
40
Pˇríklad: pˇrirozená cˇ ísla Nat
= FIX n: fnula : Unit j naslednik : ng
tj. Nat
= fnula : Unit j naslednik : Natg
je typ s hodnotami
fnula = ()g fnaslednik = fnula = ()gg fnaslednik = fnaslednik = fnula = ()ggg .. .
PB006
41
Pˇríklad: seznamy ˇ Je-li T nejaký typ, pak typ
FIX l: fnil : Unit j cons : T lg oznaˇcujeme T a
nazýváme typem všech seznamu˚ nad T . Pro a1 ; a2 ; a3 ; : : : typu T píšeme
[ ℄ = fnil = ()g [a1 ℄ = fcons = (a1; fnil = ()g)g [a1 ; a2 ℄ = fcons = (a1 ; fcons = (a2 ; fnil = ()g)g)g .. .
PB006
42
Monomorfismus a polymorfismus Monomorfní typy jsou bud’ základní typy, anebo jsou (pomocí typových konstruktoru) ˚ složené z monomorfních typu. ˚
Polymorfní typy zastupují celou množinu monomorfních typu. ˚ ˇ Parametrický polymorfismus – v typových výrazech se vyskytují typové promenné, za ˇ lze dosadit libovolný typ. než Inklusní (podtypový) polymorfismus – v typovém systému se zavede mezi typy relace
6: a každá hodnota má kromeˇ svého nejmenšího typu i všechny jeho nadtypy.
PB006
43
Parametrický polymorfismus Typ je parametricky polymorfní, zastupuje-li celou množinu monomorfních typu. ˚ Tato ˇ množina je generována náhradou typových promenných všemi monomorfními typy (v typovém výrazu reprezentujícím polymorfní typ). Parametricky polymorfní typ je vyjádˇren typovým výrazem se základními typy, typovými konstruktory a universálneˇ ˇ kvantifikovanými typovými promennými. Pˇríklady:
PB006
8b: Array (0::9) b 8a: a ! Bool 8a8b8 : fasel : a; bsel : b; sel : g 44
0
ˇ Typ T vzniklý z parametricky polymorfního typu T náhradou za nejakou jeho typovou
0
ˇ ˇ ˇ než T . promennou se nazývá odvozený z T . Ríkáme pak, že T je obecnejší
ˇ typ, z nehož ˇ Hlavní typ hodnoty v je její nejobecnejší lze odvodit pouze typy, které jsou
v souladu s definicí hodnoty v . Pˇríklady:
(x; y) = x id (x) = x fst
PB006
: 8a8b: a b ! a id : 8a: a ! a
fst
45
ˇ hodnot, jichž je T hlavním typem) je rovna Množina hodnot typu T (tj. množina tech
pruniku ˚ množin hodnot všech monomorfních typu˚ odvozených z T .
a!a a!b!a (a; b) ! b [a℄
PB006
fid g fconst g fsnd g f[ ℄g
46
Polymorfní typové systémy
8 < Girarduv-Reynolds ˚ uv ˚ s polymorfismem obecného ranku : Hindleyho-Milneruv ˚ s polymorfismem prvního ranku
Otypování výrazu je nalezení jeho (hlavního) typu. V monomorfních typových systémech je triviální. Otypování v parametricky polymorfních typových systémech je založeno na unifikaci ˇ typové systémy je obecneˇ nerozhodnutelné. typových výrazu. ˚ Pro složitejší
PB006
47
Typové systémy s podtypy Na množineˇ typu˚ je zavedeno uspoˇrádání
6: .
6: B cˇ teme „A je podtypem typu B “. Je-li A 6: B , pak v kontextu, ve kterém se oˇcekává hodnota typu B , mužeme ˚
Zápis A
bezpeˇcneˇ použít hodnotu podtypu A.
Pravidlo subsumpce Necht’ A, B jsou typy takové, že A
Potom také a je typu B .
6: B, a necht’ a je hodnota typu A.
Pravidlo subsumpce se zapisuje ve tvaru
a:A
PB006
A 6: B a:B 48
Kovariance a kontravariance Typový konstruktor S je kovariantní, když
A 6: A0 S A 6: S A0
Typový konstruktor T je kontravariantní, když
A 6: A0 T A0 6: T A
Jinak je typový konstruktor (v daném typovém parametru) invariantní. Pˇríklad:
Typový konstruktor Set je kovariantní:
6: 0 ) Set 6: PB006
Set
0
49
ˇ arity (binárních, ternárních. . . ) se kovariance a U typových konstruktoru˚ vetší kontravariance zavádí zvlášt’ pro každý typový parametr.
n-ární typový konstruktor S je ve svém i-tém typovém parametru (1 i n) kovariantní, když
Ai 6: A0 S A1 A2 : : : An 6: S A1 A2 : : : Ai 1 A0 Ai+1 : : : An
n-ární typový konstruktor T je ve svém i-tém typovém parametru (1 i n) kontravariantní, když
Ai 6: A0 T A1 A2 : : : Ai 1 A0 Ai+1 : : : An
PB006
6: T A
1
A2 : : : An
50
Pˇríklad:
Typový konstruktor
! je v prvním parametru kontravariantní a ve druhém
parametru kovariantní:
6: 0 6: 0
) 0 ! 6: ! ) ! 6: ! 0
Z kovariance druhého typového parametru a pravidla subsumpce vyplývá, že každou funkci typu
! lze považovat i za funkci nadtypu ! 0 . Tedy volání f (a), které 0
˚ objevit v kontextu, kde se oˇcekává hodnota nadtypu . vrací hodnotu typu , se muže Z kontravariance prvního typového parametru a pravidla subsumpce vyplývá, že každou
0 ! lze považovat i za funkci nadtypu ! . Tedy oˇcekává-li funkce f 0 argument typu , lze ji aplikovat na argument jeho podtypu .
funkci typu
PB006
51
Využití: zejména v typovaných systémech pro objektoveˇ orientované jazyky. Nevýhoda: nerozhodnutelnost otypování
PB006
) nutné dynamické typové kontroly.
52
Inklusní polymorfismus Též podtypový polymorfismus. Je dusledkem ˚ subsumpˇcního principu. Totiž je-li a
pak typem hodnoty a je i každý nadtyp typu A. Pˇr.:
: A,
= fx : Real; y : Realg BarevnyBod = fx : Real; y : Real; : Barvag BarevnyBod 6: Bod presun : Bod ! Bod presun fx = p; y = q g = fx = p + 1; y = q + 1g zmodrej : Bod ! BarevnyBod zmodrej fx = p; y = q g = fx = p; y = q ; = modrag
Bod
PB006
53
Potom také
fx = 2; y = 3; = zelenag : Bod presun : BarevnyBod ! Bod zmodrej : BarevnyBod ! BarevnyBod zmodrej : Bod ! Bod zmodrej : BarevnyBod ! Bod
PB006
54
Pˇretížení ˇ Symbol je pˇretížený, oznaˇcuje-li více hodnot ruzných ˚ typu. ˚ Obvykle je každá z techto ˇ hodnot definována ruzn ˚ e. Jednodušší jazyky mají pˇretížené jen zabudované operátory, jazyky s bohatšími ˇ typovými systémy ˇreší pˇretížení systematicky (napˇr. pomocí typových tˇríd) a umožnují definovat nová jména pˇretížená více hodnotami. Pˇri pˇrekladu nebo interpretaci je nutno pˇretížené symboly takzvaneˇ vyˇrešit – obdaˇrit ˇ V konkrétním výrazu se pozná, která sémantikou jediné z hodnot, jež ho pˇretežují. ˇ z techto hodnot to bude (napˇríklad z poˇctu argumentu˚ pˇretížené funkce a z jejich typu). ˚
PB006
55
U funkcí a procedur se též rozlišuje kontextoveˇ nezávislé a kontextoveˇ závislé pˇretížení. ˚ Kontextoveˇ nezávisle pˇretížené funkce a procedury lze vyˇrešit jen z typu˚ argumentu. U kontextoveˇ závisle pˇretížených funkcí (procedur) typy argumentu˚ nestaˇcí a je nutno vzít do úvahy širší kontext. ˇ Necht’ symbol g je pˇretížen dvema ruznými ˚ typy
1 ! 1 , 2 ! 2 .
V kontextoveˇ nezávislém pˇretížení (Pascal, Haskell, ML) musí být 6= . V kontextoveˇ závislém pˇretížení (Ada) je = , ale musí být 6= . Nelze je 1
1
2
1
2
2
vždy jednoznaˇcneˇ vyˇrešit. Jazyk musí nejednoznaˇcné výrazy zakazovat.
PB006
56
Pˇríklad pˇretížení Necht’ operátor
(=) : Int Int ! Int (=) : Float Float ! Float (=) : Int Int ! Float ˇ x : Float, n : Int a necht’ (=) je (rovnež
(=) je pˇretížen tˇremi typy:
Pˇretížení je kontextoveˇ závislé. Necht’
pˇretížený) operátor rovnosti vyžadující, aby obeˇ strany rovnosti byly stejného typu.
x = 7:0=2:0 x = 7=2 n = 7=2 n = (7=2)=(5=2) x = (7=2)=(5=2)
) ) ) ) ) nebo
Poslední výraz je nejednoznaˇcný, pˇretížení nelze vyˇrešit.
PB006
x = 7:0=2:0 x = 7=2 n = 7=2 n = (7=2)=(5=2) x = (7=2)=(5=2) x = (7=2)=(5=2) 57
Koerce Koerce je implicitní zobrazení hodnot jednoho typu do hodnot jiného typu.
! Float, Float ! Double, Float ! Complex a ! (a j b) (unioning) a ! () (forgetting) a ! Array i a (rowing, autoboxing) Ref a ! a (dereferencing) Int
(widening)
V moderních jazycích se od koerce upouští – interferuje s pˇretížením a polymorfismem.
PB006
58
Hodnotoveˇ závislé typy Bohatší typové systémy mohou pracovat s typy závislými na hodnotách. Typové konstruktory mohou být parametrizovány nejen typy, ale i hodnotami.
PB006
59
Pˇríklad – skalární souˇcin V jazycích bez závislých typu˚ lze test na rovnost délek násobených vektoru˚ bud’ ˇ vubec neprovádet ˚
[℄ [℄ = 0:0 dp s t = head s head t + dp (tail s) (tail t) dp
ˇ anebo ho posunout do doby behu. V jazycích se závislými typy lze korektnost zaruˇcit staticky tím, že informaci o délce vektoru zahrneme do jeho typu Vec n všech n-složkových vektoru˚ reálných cˇ ísel. Vec
:
Float
!
: 8n : Nat: Vec (n + 1) ! Float : 8n : Nat: Vec (n + 1) ! Vec n dp : 8n : Nat: Vec n ! Vec n ! Float dp [℄ [℄ = 0:0 dp s t = vhead s vhead t + dp (vtail s) (vtail t) vhead vtail
PB006
60
Pˇríklad – typ funkce printf
: String ! Printf ("%d" ++ t) = Printf ("%s" ++ t) = Printf t = Printf "" = Printf
! Printf t String ! Printf t Int
Printf t
0 ;
nezaˇcíná-li
t znakem % a t0 je zbytek
String
: (t : String) ! Printf t printf t = pr t ""; kde printf
:
printf
"ab"
printf
"%s=%d"
PB006
Printf "ab"
:
=
pr pr pr pr
"" v ("%d" ++ t) v ("%s" ++ t) v
(u ++ t) v
= v = (i:Int) 7! pr t (v ++ show i) = (s:String) 7! pr t (v ++ s) = pr t (v ++ u) ; jinak
String
Printf "%s=%d"
=
String
! Int ! String 61
Výhody hodnotoveˇ závislých typu˚ ˇ a pˇresneji. ˇ Mnoho vlastností lze závislými typy vyjádˇrit jemneji Pomocí typu˚ lze vyjádˇrit sémantiku. Potom otypování
= dukaz ˚ korektnosti.
Nevýhody Otypování je nerozhodnutelné.
Jazyky ˇ akademické jazyky: Vesmes Agda, Cayenne, Dependent ML, Russell, Epigram . . .
PB006
62
Pojetí typu˚
množiny hodnot heterogenní algebry (množiny hodnot spolu s operacemi na nich) variety heterogenních algeber (množiny s operacemi a axiomy)
PB006
algebraické typy ADT
63
Pˇríklad: Typ zásobník nad celými cˇ ísly 1. Zásobníky jsou pevným zpusobem ˚ reprezentovány, napˇríklad pomocí pole a indexu vrcholu zásobníku. Typ Zásobník má význam množiny všech takových dat (polí konkrétních hodnot + indexu). ˚ Nad zásobníky lze definovat externí operace závislé na reprezentaci.
PB006
64
2. Typ Zásobník má význam množiny všech heterogenních univerzálních algeber se signaturou Sorty:
ˇ Zásobník, Císlo, Boolean
Operace:
: Zásobník jeprázdný : Zásobník ! Boolean ˇ push : Zásobník Císlo ! Zásobník pop : Zásobník ! Zásobník ˇ top : Zásobník ! Císlo
prázdný
PB006
65
3. Typ Zásobník má význam variety všech heterogenních univerzálních algeber, která je urˇcena teorií Sorty Operace Axiomy:
( ) = True jeprázdný (push(z; n)) = False pop(push(z; n)) = z top(push(z; n)) = n jeprázdný prázdný
PB006
66
Sémantika Axiomatická sémantika Operaˇcní sémantika Denotaˇcní sémantika
PB006
67
Sémantika ( o& ) pˇriˇrazuje významy programum ˚ nebo jejich cˇ ástem. Sémantiku programovacího jazyka lze zadat
Neformálneˇ – popisem v pˇrirozeném jazyce. To muže ˚ být nepˇresné, cˇ asto je popis neúplný, nejednoznaˇcný.
Prohlášením jedné implementace kompilátoru za standard. Sice jednoznaˇcné, ale pˇrípadné chyby v kompilátoru se tak stávají souˇcástí definice jazyka.
Formálne,ˇ pomocí matematického zápisu.
PB006
68
Formální sémantika ˇ sémantika je definovaná na programech a jejich komponentách explicitneˇ Denotacní (jako množina funkcí pˇriˇrazujících cˇ ástem programu˚ význam). ˇ sémantika se zavádí množinou pravidel popisujících výpoˇcet abstraktního Operacní poˇcítaˇce. Výsledek tohoto výpoˇctu je významem programu. ˇ Axiomatická sémantika je dána jako množina tvrzení (tzv. teorie) o nejakém systému, ˇ v nemž probíhá výpoˇcet. Používá se zejména u imperativních jazyku, ˚ protože tvrzení se vyjadˇrují o stavech.
PB006
69
Denotaˇcní sémantika – pˇríklad
P
množina programových konstrukcí (v abstraktní syntaxi)
MVar
ˇ množina programových (pˇrepisovatelných) promenných
V S = MVar ! V [ _℄ _ : P S ! S M[ _℄ _ : P S ! V
[ x ++℄ = 0,
kde
M[ x ++℄ = (x) PB006
množina hodnot množina stavu˚ stavový transformátor významová funkce
0 (x) = (x) + 1 8y; y 6= x: 0(y) = (y)
70
Operaˇcní sémantika – pˇríklad Relace „krok výpoˇctu“
(P S ) (P S ) je zadána množinou pravidel.
he; i htt ; 0 i hif e then p else q; i hp; 0 i he; i hff ; 0 i hif e then p else q; i hq; 0 i he; i he0 ; 0i hif e then p else q; i hif e0 then p else q; 0i PB006
71
Axiomatická sémantika – pˇríklad Sekvent v Hoaroveˇ logice je trojice tvaru
fAg p fB g, kde A je tzv. vstupní podmínka,
B je výstupní podmínka a p je pˇríkaz. Množina odvoditelných sekventu˚ je zadána odvozovacími pravidly a axiomy.
f[e= ℄Ag x := e f[!x= ℄Ag fAg p fB g; B C; fC g q fDg fAg begin p;q end fDg fA ^ eg p fAg fAg while e do p fA ^ :eg PB006
72
Denotaˇcní sémantika Pˇriˇrazení prvku˚ sémantických domén programovým konstrukcím Syntaktickéentity: termy(ajejich konstruktory) zabstraktní syntaxe
Sémantickéentity: prvkysémantických domén
0 42
0
1
1
42
(1+) or
successor
6*7 succ True ()
tt
v ff
0
not
PB006
73
Nedeterministická sémantika Pˇríkazy urˇcují nedeterministické stavové transformátory:
s : S ! P (S ) Sekvence
[ begin end℄ = fg [ [ begin p1 ; : : : ; p end℄ = f[ p ℄ j 2 [ begin p1 ; : : : ; p k
PB006
k
k
℄ g pro k 1 1
end
74
ˇ Nedeterministický výber
[ begin p1 j : : : j p
k
℄ =
end
k [
[p ℄ i
i=1
Paralelní kompozice
[ begin p1 jj : : : jjp
k
end
℄ =
[
[ begin p (1); : : : ; p ( ) end℄
k
permutace
pro atomické p1 ; : : : ; pk
PB006
75
Deterministická sémantika Významem výrazu e je jeho hodnota (prvek sémantické domény). V imperativních jazycích závisí sémantika výrazu na stavu
2 S , takže
M[ e℄ : S ! Val Význam výrazu e ve stavu je hodnota M[ e℄ 2 Val. ˇ V jazycích bez vedlejších efektu, ˚ ale s (ˇcistými) promennými závisí sémantika výrazu na
2 Env . Potom M[ e℄ : Env ! Val Význam výrazu e v hodnotovém kontextu " je hodnota M[ e℄ " 2 Val. tzv. hodnotovém kontextu "
PB006
76
Sémantika výrazu˚ se definuje pomocí sémantiky podvýrazu. ˚ Pˇríklad:
M[ 0℄ = 0 M[ 1℄ = 1 .. .
M[ e + e ℄ = M[ e ℄ + M[ e ℄ M[ e * e ℄ = M [ e ℄ M[ e ℄ 8 > > M[ e ℄ ; pokud M[ e ℄ = true > < M[ if e then e else e ℄ = > M[ e ℄ ; pokud M[ e ℄ = false > > : ? jinak 1
PB006
2
1
2
1
1
2
1
3
2
2
2
1
3
1
77
Výrazy Literály oznaˇcují hodnoty a obvykle jsou tvoˇreny jediným lexikálním atomem se zvláštní lexikální syntaxí, napˇríklad 42, 1.602e–19, 0xBE, ’*’, ’\n’. Jména
(pojmenované) konstanty: pi ; sin parametry funkcí ˇ (pˇrepisovatelné) promenné Výrazy popisující hodnoty složených typu˚
(1; ’a’); fjmeno = "Bob"; adresa = "klobouk"g
PB006
78
ˇ Podmínené výrazy if : : : then : : : else,
case : : : of : : :
Aplikace funkce na argumenty, tzv. „volání funkce“. ˇ Abstrakce („uzávery“). Pˇríkazy v imperativních jazycích lze považovat za zvláštní druh výrazu (výraz typu Command).
PB006
79
Funkcionální a procedurální abstrakce V mnoha jazycích lze funkcionální/procedurální abstrakci použít jen v definicích funkcí/procedur, ale napˇr. v Algolu68 je lze použít i ve výrazech/pˇríkazech a ve ˇ e. ˇ funkcionálních jazycích se funkcionální abstrakce (lambda abstrakce) užívají bežn Tzv. procedury lze považovat za funkce typu t1 Pˇr.: repeat mezery repeat mezery
PB006
: : = =
( Procedure(Int);
t ! Command.
Procedure Int; Command
n
);
(n : Int; p : Command)ffrom 1 to n do pg proc(n : Int)fif n 0 then repeat (n; write(’ ’)) else repeat ( n; write (’\0x08’))g proc
80
ˇ ˇ Funkcionální abstrakce se provádí nad výrazem tím, že nekteré jeho (volné) promenné ˇ se prohlásí za parametry výsledné funkce. Poˇcet techto parametru˚ urˇcuje tzv. aritu. ˇ Umožnuje-li jazyk pracovat s funkcemi vyšších ˇrádu, ˚ lze všechny funkce (procedury) pˇrevést na unární. Podobneˇ procedurální abstrakce se provádí nad pˇríkazem.
) xx = \x! xx
ML:
val sqr
Haskell:
sqr
Lisp: Pascal: C:
=
fn x
(define sqr (lambda (x) ( x x))) function sqr (x : real) : real; begin sqr := x x end float sqr (float x) freturn x x; g
Princip abstrakce lze zobecnit i na jiné syntaktické kategorie, než funkce (napˇr. na typovou abstrakci apod.). PB006
81
ˇ Promenné Rozdílný význam v ruzných ˚ paradigmatech: ˇ ˇ Funkcionální, logické – cˇ isté promenné, promenné v matematickém smyslu. ˇ Promenná oznaˇcuje hodnotu (tˇrebaže pˇredem neurˇcenou). Slouží také k oznaˇcení parametru˚ funkcí resp. relací. Haskell: Prolog:
PB006
0 then 1 else n fact (n 1) lessthan(succ (X ); succ (Y )) :- lessthan(X; Y ):
fact
n =
if n ==
82
ˇ Imperativní – tzv. pˇrepisovatelné promenné. ˇ ˇ ˇ Promenná oznaˇcuje pamet’ové místo. Teprve toto pamet’ové místo slouží jako ˇ ˇ (pˇrechodné) úložišteˇ hodnoty. Hodnota uložená v pamet’ovém místeˇ se muže ˚ menit. ˇ stav výpoˇctu. Tím se mení ˇ ˇ Ve vetšin eˇ imperativních jazyku˚ (Pascal, C, Java, . . . ) se však jménem promenné ˇ oznaˇcuje i hodnota uložená v odpovídajícím pamet’ovém místeˇ (automatické dereferencování). Pascal: Algol68: ML:
PB006
(n); n := n + 1; write(n) end Ref Int n; n := n + 1 n : int ref; n := !n + 1
begin read
83
ˇ ˇ komponent. Pˇrepisovatelné promenné složených typu˚ mohou mít tzv. selektivní zmeny Datum
= fr : Int; m : String; d : Intg
: Ref Datum dnes := fr = 2005; m = "°íjen"; d = 5g dnes :d := dnes:d + 1 dnes
dnes := fr = (!dnes ):r ; m = (!dnes ):m; d = (!dnes ):d + 1g
PB006
84
Datum’
= fr : Ref Int; m : Ref String; d : Ref Intg
: Datum’ dnes = fr = ref 2005; m = ref "°íjen"; d = ref 5g dnes :d := dnes:d + 1 dnes
dnes :d
PB006
:= !(dnes:d) + 1
85
rdnes
: Ref Datum’
rdnes
:= dnes
rdnes :d
:= rdnes:d + 1
(!rdnes):d := !((!rdnes):d) + 1
PB006
86
Pˇríkazy Významem pˇríkazu je stavový transformátor MVar
s:S
!S
ˇ ˇ množina programových promenných representujících pamet’ová místa (i persistentní data)
Val
ˇ množina hodnot, jež mohou být do techto míst uloženy
: MVar ! Val stav S množina všech stavu˚ Je-li p pˇríkaz, pak jeho stavový transformátor se znaˇcí [ p℄ : S
PB006
! S.
87
Pˇríkazy obsahující výrazy bez vedlejších efektu˚ ˇ stav, výrazy stav nemení. ˇ Pˇredpokládejme pro zaˇcátek, že pouze pˇríkazy mení Prázdný pˇríkaz skip
[ skip℄ = id ; [ skip℄ = pro všechny stavy 2 S Pˇriˇrazovací pˇríkaz v
:= e
[ v := e℄ = 0;
0 (v ) = M[ e℄ ; 8x 2 MVar fvg: 0(x) = (x)
kde
M[ e℄ je hodnota výrazu e ve stavu
PB006
88
Sekvence begin p1
;:::;p
k
end
[ begin p1 ; : : : ; p
k
tj. pro všechna
end
k
2S
[ begin p1 ; : : : ; p
k
end
℄ = [ p ℄ ([[p
ˇ pˇríkaz if e then p1 else p2 Podmínený
k
8 > > > <
[ if e then p1 else p2℄ = > > > :
PB006
℄ = [ p ℄ Æ Æ [ p1 ℄ k
1
℄ (: : : ([[p2 ℄ ([[p1 ℄ )) : : :))
[ p1 ℄ ; pokud M[ e℄ = true [ p2 ℄ ; pokud M[ e℄ = false
? jinak
89
Pˇríkaz cyklu while e do p
8 > > > <
;
> > :
? jinak
pokud
M[ e℄ = false
[ while e do p℄ = > [ while e do p℄ ([[p℄ ); pokud M[ e℄ = true Tvrzení: Pro každý výraz e a pˇríkaz p platí
[ while e do p℄ = [ if e then begin p; while e do p end℄ Dukaz ˚ dosazením do definice [[_℄℄.
PB006
90
ˇ Násobné vetvení case e of
v1 ! p1 v2 ! p2 .. .
vk ! pk
[ case e of v1 ! p1 ; : : : ; v ! p ℄ = [ p ℄ ; kde i = minfj j1 j k; M[ v ℄ = M[ e℄ g; k
k
i
j
existuje-li toto minimum, jinak
PB006
91
Výrazy s vedlejšími efekty Pˇripustíme, aby pˇríkazy (tj. výrazy typu Command) byly podvýrazy výrazu˚ jiného typu. Pak jsou všechny výrazy stavovými transformátory vracejí hodnotu
M[ e℄ : S ! Val.
Napˇríklad v C ve stavu ;
[ e℄ : S ! S , ale kromeˇ toho
(x) = 5, je
[ x ++℄ = 0; 0(x) = 6; 0(y) = y pro y 6= x M[ x ++℄ = 5
PB006
92
[ skip℄ = id [ x := e℄ = 0;
[e
l
:= er ℄
x 2 MVar 0 (x) = M[ e℄ 0 (y) = ([[e℄ )(y)
= 0;
[ begin p1 ; : : : ; p
k
PB006
pro y
2 MVar fxg
v = M[ el ℄ ([[er ℄ ) 0(v) = M[ er ℄ 0(y) = ([[el ℄ ([[er ℄ ))(y) end
pro y
2 MVar fvg
℄ = [ p ℄ Æ Æ [ p1 ℄ k
93
8 > > > <
[ if e then p1 else p2℄ = > > > :
8 > > > <
[ while e do p℄ = > > > :
PB006
[ p1 ℄ ([[e℄ ); [ p2 ℄ ([[e℄ );
? jinak
M[ e℄ = true pokud M[ e℄ = false pokud
[ e℄ ; pokud M[ e℄ = false [ while e do p℄ ([[p℄ ([[e℄ )) ; pokud M[ e℄ = true
? jinak
94
ˇ Radicí pˇríkazy Skoky Explicitní pˇrenesení ˇrízení výpoˇctu do jiné cˇ ásti programu. Obvyklé ve starších jazycích ˇ Vetšina ˇ a jazycích nižší úrovne. jazyku˚ klade na použití skoku˚ omezení (napˇríklad je možný jen skok do stejného nebo nadˇrazeného bloku). ˇ Pˇrílišné používání skoku˚ vede k neˇcitelnému kódu a težko odhalitelným chybám. Napˇríklad
PB006
go to v C
95
Úniky ˇ složeného pˇríkazu, který únikový pˇríkaz obsahuje. Ukonˇcují provádení ˇ nejvnitˇrnejší ˇ n-tý nejvnitˇrnejší
exit n
ˇ urˇcitého druhu (cykly, case) nejvnitˇrnejší
C: continue, break, Prolog: !
ˇ funkcionální cˇ i procedurální abstrakce nejvnitˇrnejší celý program
PB006
C: return
halt, Fortran: stop, sh: exit
96
Výjimky Mohou být ošetˇreny procedurou pro zpracování výjimky (tzv. handler). Výjimek muže ˚ být více, ruzných ˚ typu, ˚ a pro každou muže ˚ být definováno jiné zpracování; ruzné ˚ cˇ ásti programu mohou definovat ruzná ˚ zpracování stejné výjimky. Není-li výjimka zpracována (ošetˇrena), je šíˇrena (propagována) do pˇríkazu nadˇrazeného. ˇ Nekteré výjimky jsou zabudované a vyvolávané zabudovanými operacemi, jiné lze uživatelsky definovat a vyvolat zvláštním pˇríkazem (ML: raise, Java: throw). Oblast zpracování (scope) výjimky je vymezena programovým blokem nebo zvláštní syntaxí (try. . . end).
PB006
97
Volání funkcí a pˇredávání parametru˚ aplikace funkce (procedury) na argumenty – tzv. volání funkce (procedury). Volání hodnotou – striktní vyhodnocení Volání jménem – normální vyhodnocení Volání dle potˇreby – líné vyhodnocení (v referenˇcneˇ transparentních jazycích). Volání odkazem (referencí) Volání hodnotou, výsledkem, hodnotou-výsledkem.
PB006
98
Definice funkce (procedury)
f (x1 ; : : : ; xn ) = b x1 ; : : : ; xn
levá strana – hlaviˇcka jsou formální parametry
ˇ pravá strana – telo výraz nebo pˇríkaz
Aplikace funkce (procedury) na argumenty neboli volání funkce (procedury)
f (a1 ; : : : ; an ) argumenty (výrazy)
PB006
99
Volání hodnotou
f (x1 ; : : : ; xn ) = b f (a1 ; : : : ; an ) , kde a1 ; : : : ; an jsou výrazy.
Necht’ definice funkce (procedury) je a její volání je
[ f (a1 ; : : : ; a )℄℄ = [ b℄ 0 M[ f (a1 ; : : : ; a )℄℄ = M[ b℄ 0
Pak
n
kde pro všechna i;
1in
0 i 0 (xi ) 0 (y ) PB006
= = = =
n
[ ai℄ i 1 M[ ai ℄ i 1 n (y) pro každé y 2= fx1 ; : : : ; xn g 100
Volání jménem Necht’ definice funkce f je
Pak
f (x1 ; : : : ; xn ) = b
[ f (a1 ; : : : ; a )℄℄ = [ b0 ℄ M[ f (a1 ; : : : ; a )℄℄ = M[ b0 ℄ n
n
0
kde b vznikne z b souˇcasnou substitucí výrazu˚ a1 ; : : : ; an za všechny (volné) výskyty
formálních parametru˚ x1 ; : : : ; xn , tj.
b0 = [a1 =x1 ; : : : ; an =xn ℄b
PB006
101
Volání jménem se implementuje pomocí nulárních (bezparametrických) funkcí pro každý skuteˇcný parametr pˇredávaný jménem – tzv. thunks. Pˇr.:
( : Ref Int; m : Int; n : Int; name x : Real) : Real s : Ref Real; s := 0; for i := m to n do s := (s) + x ;
function sum i = begin
return (s ) end; k : Ref Int; .. .
( 1; 10; 1=(k (k + 1)))
sum k ;
PB006
102
C:
double sum ( int *i, int m, int n, double (*x)() ) { double s; s = 0; for (*i = m; *i <= n; (*i)++) { s = s + (*x)(); } return s; } ... double thunk1 (void) { return 1/(k*(k+1)); } ... sum (&k, 1, 10, &thunk1); PB006
103
Volání „dle potˇreby“ – líná aplikace Varianta volání jménem. Argumenty se však vyhodnocují nejvýše jednou. Používá se jen u referenˇcneˇ transparentních jazyku, ˚ tedy u jazyku˚ bez vedlejších efektu. ˚
PB006
104
Volání odkazem ˇ být jen Podobné volání hodnotou, ale skuteˇcné parametry funkcí a procedur smejí ˇ (adresovatelná) pamet’ová místa (Ref T) a neprovádí se jejich implicitní dereferencování. ˇ Formální parametry jsou nepˇrepisovatelné promenné typu „odkaz na hodnotu“ (Ref T) – napˇr. v Pascalu. Pˇri simulaci pomocí volání hodnotou (napˇr. v C) mohou být formální parametry ˇ ˇ pˇrepisovatelné promenné uchovávající pˇrepisovatelné promenné (Ref (Ref T)) – dereferencování je pak dvojnásobné.
PB006
105
Pascal: var a; b
: Real;
var z
: Real;
(
procedure swap var x; y begin
z := x; x := y; y := z
: Real);
a; b : Ref Real x; y : Ref Real z : Ref Real z := (x) x := (y) y := (z )
end; .. . swap
(a; b)
swap
(a; b)
Implicitnímu dereferencování pˇri volání zabrání zpusob ˚ pˇredávání parametru. ˚
PB006
106
C:
double a,b; void swap (double *x, double *y) { double z; z = *x; *x = *y; *y = z; } ... swap (&a,&b)
a,b x,y z z *x *y
: Ref Real : Ref (Ref Real) : Ref Real := (*x) := (*y) := (z)
Implicitnímu dereferencování pˇri volání zabrání statický operátor & – hodnotou se pˇredají adresy
PB006
107
Volání výsledkem ˇ Skuteˇcnými parametry mohou být jen výrazy typu Ref a, tj. adresovatelná pamet’ová ˇ místa (napˇr. pˇrepisovatelné promenné, prvky pˇrepisovatelných datových struktur . . . ). Je-li definice funkce (procedury)
f (out y1 ; : : : ; yn ) = b Pak
[ f (w1 ; : : : ; w )℄℄ = 00 M[ f (w1 ; : : : ; w )℄℄ = M[ b℄ n
n
kde pro všechna i;
PB006
1in
i vi 0 00(vi ) 00(u)
= = = = =
n
[ w ℄ 1; 0 = M[ w ℄ 1 [ b℄ 0 (y ) 0 (u) pro u 2= fv1 ; : : : ; v g i
i
i
i
n
i
n
108
Volání hodnotou-výsledkem ˇ Skuteˇcnými parametry mohou být jen adresovatelná pamet’ová místa.
f (inout z1 ; : : : ; zn ) = b [ f (w1 ; : : : ; wn )℄℄ = 000 M[ f (w1 ; : : : ; wn )℄℄ = M[ b℄ 0
Je-li definice procedury (funkce) Pak
kde pro všechna i;
PB006
1in
i vi 0 (zi ) 0 (u) 00 000(vi ) 000(u)
= = = = = = =
[ w ℄ 1; 0 = M[ w ℄ 1 (v ) (u) pro u 2= fz1 ; : : : ; z g [ b℄ 0 00(z ) 00(u) pro u 2= fv1 ; : : : ; v g i
i
i
n
i
i
n
n
i
n
109
Smíšené volání – hodnotou, výsledkem, hodnotou-výsledkem Jazyky, které podporují volání hodnotou, výsledkem, hodnotou-výsledkem, zpravidla dovolují, aby jedna víceparametrická funkce (procedura) své parametry vyhodnocovala ruznými ˚ zpusoby, ˚ podle pˇredpisu v hlaviˇcce funkce (procedury).
f (in x1 ; : : : ; xm ; out y1 ; : : : ; yn ; inout z1 ; : : : ; zr ) = b
PB006
110
Volání odkazem a volání hodnotou-výsledkem mají ruznou ˚ sémantiku. ˇ ˇ obsah pˇrepisovatelné promenné ˇ Když se behem zpracování funkce cˇ i procedury mení ˇ se souˇcasneˇ obsah urˇcené formálním parametrem pˇredávaným odkazem, mení ˇ pˇrepisovatelné promenné, která je skuteˇcným argumentem pˇri volání. ˇ obsah pˇrepisovatelné promenné ˇ Naproti tomu, když se mení urˇcené formálním ˇ se tyto zmeny ˇ pouze lokálneˇ a parametrem pˇredávaným hodnotou-výsledkem, dejí ˇ až v okamžiku návratu. obsah skuteˇcného argumentu se zmení Tento rozdíl muže ˚ mít (zejména pˇri neˇcistém stylu programování) vliv na výsledný stav. var a; b : Int; function f (ref=inout x : Int) : Int { x := 1; a := a + 1; return x;
}
:= 1; b := f (a);
a
PB006
111
Viditelnost
PB006
112
Viditelnost jazykových entit Statická ˇ Pro každou definici jazykové entity (konstanty, promenné, typu, . . . ) je tzv. statickou sémantikou urˇcena oblast platnosti definice. Blokové jazyky (Pascal, Modula, Algol68, . . . ) Stromová struktura. Globální a lokální entity. Modulární jazyky (C, Modula, . . . ) Moduly se vzájemneˇ nevnoˇrují, ale mohou být tvoˇreny blokem. Tˇrídy viditelnosti: public / private. Objektové jazyky – z hlediska viditelnosti podobné modulárním, rozlišují tˇrídy a objekty. Amorfní jazyky (Basic) Nepoužitelné pro „programování ve velkém“. PB006
113
Dynamická Viditelnost jazykových entit závisí na momentálneˇ aktivních programových jednotkách ˇ (blocích, funkcích, procedurách, . . . ) v dobeˇ behu. ˇ r nepoužívaná (Lisp, Snobol, APL). Témeˇ
PB006
114
M
M A C D
B
A C
D viditelnost
B
PB006
115
Oblast pusobnosti ˚ (scope) v jazycích s blokovou viditelností je podobná jako v matematickém zápisu:
8x 2 A 9f :A ! B: f (x) = b ^ 8x 2 A: f (x) b Množina pojmenováných entit známých v dané oblasti pusobnosti ˚ zhruba odpovídá pojmu jmenný prostor. Avšak: ˇ (i) nekteré jazyky mohou se jmennými prostory zacházet explicitneˇ a nezávisle na jmenných prostorech implicitneˇ urˇcených bloky nebo moduly (C++); ˇ (ii) jmenné prostory mohou být rozdeleny na disjunktní cˇ ásti podle druhu˚ ˇ pojmenovávaných entit – jména pro promenné zvlášt’, jména pro typy zvlášt’, jména pro moduly zvlášt’, . . . (Haskell).
PB006
116
M useA,B(t)
A
privateu,x,z
B
useC(t)
useC(t,u)
publicp,q,r
publicr,s,t
privatex,y,z
C
privatex,y,p,q
publicy,z,t,u private...
PB006
117
Dynamická viditelnost v Lispu
(define (f (lambda (x) (+ x y)))) (define (g (lambda (y) (* (f 2) y)))) (define (h (lambda (y) (+ (f y) (g (f 5)))))) (h 2) (+ (f 2) (g (f 5)))
y=2 x=2
(+ (+ 2 2) (g (f 5))) (+ 4 (g (f 5)))
x=5
(+ 4 (g (+ 5 2))) (+ 4 (g 7)) (+ 4 (* (f 2) 7))
y=7 x=2
(+ 4 (* (+ 2 7) 7)) 67 PB006
118
Omezování viditelnosti – zapouzdˇrení Moduly Ada: package ph is
: constant Float = 3e8 G: constant Float = 6.7e–11 h: constant Float = 6.6e–34
end ph definuje uspoˇrádanou trojici
( ; G; h), ale její selektory jsou viditelné jen lokálne,ˇ tj. ,
G, h jakožto funkce mají jednoprvkový definiˇcní obor fphg. Zápis: ph: , ph:G, ph:h. Na rozdíl od agregátu˚ (uspoˇrádaných n-tic) mohou mít moduly i lokálneˇ definované typy (popˇrípadeˇ jiné jazykové entity). Typy i data mohou být privátní (neexportovatelné) a veˇrejné (exportovatelné). PB006
119
Tˇrídy a objekty Objekt ˇ je modul se skrytými (privátními) pˇrepisovatelnými promennými (tzv. atributy) a ˇ ˇ s veˇrejnými operacemi (tzv. metodami) nad temito promennými .
Tˇrída („generický objekt“) popisuje typ objektu. Vlastní objekty se nazývaji instance tˇrídy a vytváˇrejí se zvlášt’:
deklarací – statické objekty pˇríkazem – dynamické objekty Definice tˇrídou exportovaných atributu˚ a metod je souˇcástí
definice tˇrídy – statické metody, pˇrípadneˇ atributy ˇ deklarace instance – atributy, nekdy i metody PB006
120
ˇ cnost Dediˇ
6: ). ˇ metody tˇrídy B a pˇrípadneˇ Tˇrída A je podtˇrídou tˇrídy B (znaˇcíme A 6: B ), když dedí mezi tˇrídami je zavedena relace podtˇríd ( pˇridává další.
ˇ cnost je jednoduchá, má-li každá tˇrída nejvýše jednu bezprostˇrední nadtˇrídu. Jinak Dediˇ ˇ cnost násobná. je dediˇ
PB006
121
Vlastnosti OO jazyku˚ Tˇrídy a objekty (statické nebo dynamické). ˇ cnost a inkluzní polymorfismus Dediˇ
typový systém s podtypy a : A; A 6: A0 ) a : A0 Viditelnost omezená na objekty a ˇrízená pomocí public / private (pˇríp. protected). V (dynamických) objektech mohou být atributy i metody
statické – definované ve tˇrídách dynamické – definované v objektech PB006
122
OO jazyky ˇ Simula 67 považována za nejstarší OO jazyk, poprvé se v ní objevily nekteré principy OO programování Smalltalk cˇ isteˇ objektový, prototyp OO jazyku; ˚ netypovaný Eiffel cˇ isteˇ objektový, typovaný C++ puvodn ˚ eˇ jen rozšíˇrení C pomocí makrojazyka cpp, není cˇ isteˇ objektové ˇ Java spolu s C++ nejrozšíˇrenejší, není cˇ isteˇ objektová (má primitivní typy, které nejsou tˇrídami), ale má cˇ istší design než C++ Python, Ruby interpretovaný bytový kód Modula 3, Ada 95, OCaML, . . .
PB006
123
ˇ Správa pameti
PB006
124
ˇ Pamet’ové tˇrídy dat Persistentní data existují nezávisle na výpoˇctu, jsou spravována souborovým podsystémem operaˇcního ˇ ˇ ˇ systému. Obvykle jsou umístena na vnejších pamet’ových médiích (soubory, databáze).
Transientní data ˇ existují pouze po dobu výpoˇctu. Jsou obvykle umístena v dostupné (procesem ˇ (hodnoty promenných, ˇ adresovatelné) cˇ ásti operaˇcní pameti parametru, ˚ obsahy ˇ pˇrepisovatelných promenných, . . . ), ale i vneˇ (doˇcasné soubory, data na portech, . . . ). ˇ zpracování procesu˚ je rozlišení dat na persistentní a transientní V prostˇredí soubežného relativní.
PB006
125
ˇ Pamet’ová transientní data:
Statická Automatická (zásobníková) Dynamická (haldová)
PB006
126
ˇ Správa pameti Statická ˇ provádená pˇrekladaˇcem (statická data, tˇrída static, own). ˇ ...] [instrukce programu, systémová data, statická data, vyrovnávací pameti,
Zásobníková v dobeˇ výpoˇctu pˇri zahájení/ukonˇcení aktivace procedury, bloku, aplikace funkce na argumenty (automatická data, tˇrída auto). [lokální data v blocích, parametry funkcí a procedur, pomocné datové struktury ve funkcích, návratové adresy, . . . ]
Dynamická ˇ v dobeˇ výpoˇctu, provádená speciálními procedurami pro alokaci, dealokaci, pˇresouvání, scelování, . . . (dynamická data, tˇrída dynamic). 1. ˇrízená explicitneˇ programem
[malloc, free, new, dispose, mark, release]
ˇ 2. spouštená výhradneˇ „run-time podporou“ výpoˇctu
PB006
[garbage collecting, setˇrásání] 127
ˇ Fáze správy pameti ˇ alokace (pˇridelení) ˇ dealokace (uvolnení) ˇ muže obnovení volné pameti ˚ vyžadovat gc ˇ scelování – zmena polohy obsazených a volných bloku˚
cˇ ásteˇcné úplné
PB006
128
Problémy:
smetí () gc) slepé odkazy fragmentace () cˇ ásteˇcné scelování)
PB006
129
ˇ Správa dynamické pameti Inicializace vytvoˇrení seznamu volných bloku, ˚ seznamu mimohaldových ukazatelu˚ volnébloky
PB006
130
Alokace bloku požadované velikosti volnébloky
volnébloky
11111111 00000000 00000000 11111111 00000000 11111111 00000000 11111111 00000000 11111111
PB006
131
ˇ bloku Uvolnení nekorektní – vznik slepého odkazu volnébloky
nekorektní – vznik smetí volnébloky
11111111 00000000 00000000 11111111 00000000 11111111 00000000 11111111 00000000 11111111
PB006
132
Úklid smetí (garbage collection)
každý alokovaný blok má pˇríznak dostupnosti (1 bit) všechny pˇríznaky dostupnosti se nastaví na „nedostupné“ postupuje se od známých ukazatelu˚ a všechny navštívené bloky se oznaˇcí ˇ eˇ bloku již oznaˇceného za „dostupný“ se hloubeji ˇ „dostupné“ (pˇri návštev nepokraˇcuje)
nakonec se všechny nedostupné bloky zaˇradí do seznamu volných
PB006
133
Scelování (spojování sousedních volných bloku) ˚ je snazší, pokud se seznam volných bloku˚ udržuje uspoˇrádaný podle adres volnébloky
PB006
134
Setˇrásání (úplné scelování) ˇ ukazatelu˚ zpusobí ˚ zmeny volnébloky
PB006
135
Paradigmata
PB006
136
Deklarativní paradigmata Program popisuje, co je výsledkem. Funkcionální – program je výraz a výpoˇcet je jeho úprava. Logické – program je teorie a výpoˇcet je odvození z ní.
Imperativní paradigmata ˇ k výsledku. Program popisuje, jak se dospeje ˇ procedur nad daty. Procedurální – výpoˇcet je provádení Objektové – výpoˇcet je pˇredávání zpráv mezi objekty.
PB006
137
Logické paradigma Patˇrí mezi deklarativní paradigmata. Logické programy popisují vztahy mezi hodnotami pomocí tzv. Hornových klausulí. Program se skládá ze seznamu klausulí (teorie) a z formule (cíle, dotazu). Výpoˇcet je ˇ ˇ hledáním tzv. splnujících substitucí, tj. takových ohodnocení promenných z cíle, pˇri nichž cíl vyplývá (lze odvodit) z teorie. Abstraktní syntax prototypového logického jazyka: Program Klausule Formule Term
::= ::= ::= ::=
Klausule Formule Formule
(
:- Formule
Pred Term Var
)
j Fun (Term )
ˇ Pred, Fun, Var oznaˇcují predikátové symboly, funkˇcní symboly a promenné. PB006
138
Kontextová omezení (Statická sémantika) Predikátové a funkˇcní symboly mají konsistentní arity, tj.
\ : ' = P (t ; : : : ; t ) ) n = a 8P 2 [ Pred 9! a 2 N 8' 2 Formule
9! a 2 N 8t 2 [ Term: t = F (t ; : : : ; t ) ) n = a 8F 2 Fun 1
1
PB006
n
n
139
( ): Rodiˇc (Jan; Karel ): Rodiˇc (Jan; Petr ): Rodiˇc (Jana; Alena): Rodiˇc (Karel ; Alena): Sourozenec (x; y ) :- Rodiˇc (z; x); Rodiˇc (z; y ): Potomek (x; y ) :- Rodiˇc (y; x): Potomek (x; y ) :- Rodiˇc (y; z ); Potomek (x; z ): Rodiˇc Marie; Karel
ˇ implikace se nazývá hlava klausule. Levá strana (tj. záver) Pˇredpoklady implikace se nazývají podcíle. Klausule s nulovým poˇctem podcílu˚ je tzv. fakt.
PB006
140
ˇ ˇ jsou implicitneˇ Promenné v klausuli, které se vyskytují na levé straneˇ klausule (v hlave), ˇ univerzálneˇ kvantifikovány. Ostatní promenné v klausuli (ty, jež se vyskytují jen na pravé ˇ straneˇ – v podcílech) jsou implicitneˇ existenˇcneˇ kvantifikovány. (Promenné jsou tedy v klausulích lokální!) Napˇr.
PB006
8x 8y : Potomek (x; y) ( 9z : Rodiˇc(y; z) ^ Potomek (x; z)
141
Potomek(Alena,Jan)
Rodic(Jan,Alena) Rodic(Jan,z),Potomek(Alena,z) Rodic(Jan,Karel),Potomek(Alena,Karel) Rodic(Karel,Alena) Rodic(Karel,z’),Potomek(Alena,z’) Rodic(Karel,Alena),Potomek(Alena,Alena) Rodic(Alena,Alena) Rodic(Alena,z’’),Potomek(Alena,z’’) Rodic(Jan,Petr),Potomek(Alena,Petr) Rodic(Petr,Alena) Rodic(Petr,z’’),Potomek(Alena,z’’)
PB006
142
Termy Zero – nulární funkˇcní symbol (konstanta) Succ – unární funkˇcní 9symbol
Succ
Succ Zero
> > > > > > = uzavˇrené
.. .
> > termy > > > > ;
.. .
Zero
( ) Succ (Succ (Zero ))
(x) Succ (Succ (Succ (z )))
9 > > > = termy > > ˇ s promennými > ;
Klausule
( (y)): LessThan(Succ (x); Succ (y )) :- LessThan(x; y ): LessThan Zero ; Succ
Dotaz LessThan PB006
(x; Succ (Succ (Zero))): 143
Pˇríklad: ternární relace spojování seznamu˚
( ): Append (Cons (x; s); t; Cons (x; u)) :- Append (s; t; u): Append Nil ; y; y
(
(
(
Append Nil ; Cons A; Cons B ; Nil
)); Cons(B; Cons(A; Nil )))
no.
(
(
Append Cons A; Nil
); Nil ; Cons(A; Nil ))
yes.
PB006
144
( ): Append (Cons (x; s); t; Cons (x; u)) :- Append (s; t; u): Append Nil ; y; y
Append
(v; Cons(B; Nil ); Cons(B; Cons(B; Nil ))) v = Cons(B; Nil ): (
(
Append Cons A; Nil
); w; Nil )
no.
Append
PB006
(v; Cons(B; Nil ); Cons(A; Cons(x; Nil ))) v = Cons(A; Nil ); x = B: 145
( ): Append (Cons (x; s); t; Cons (x; u)) :- Append (s; t; u): Append Nil ; y; y
Append
PB006
(v; w; Cons(A; Cons(B; Nil ))) v = Nil ; w = Cons(A; Cons(B ; Nil )); v = Cons(A; Nil ); w = Cons(B; Nil ); v = Cons(A; Cons(B; Nil )); w = Nil :
146
Sémantika logického programu Substituce Subst je množina všech substitucí, tj. koneˇcných zobrazení Var kde GTerm
!
f
GTerm
ˇ = f 2 Term j neobsahuje promenné g je množina všech tzv.
uzavˇrených termu. ˚ Každou substituci
: Term
: Var ! GTerm lze jednoznaˇcneˇ homomorfneˇ rozšíˇrit na termy,
! GTerm
(v) = (v) (g) = g (f (t1 ; : : : ; tn )) = f ((t1 ); : : : ; (tn ))
(p) = (q).
Unifikátor formulí p; q je substituce taková, že PB006
147
Sémantika
M[ _℄ :
! P (Subst ) M[ ( ; q)℄℄ = f 2 Subst j ` (q); 8D $ Dom : 0 j (q)g Pˇritom ` je relace tzv. odvoditelnosti cíle definovaná: Programy
D
= [ f1;0 :- f1;1 ; : : : ; f1;m1 .. .
fn;0 :- fn;1 ; : : : ; fn;mn ℄ ` q
, 9 2 Subst 9i; 1 i n: (q) = (f ) ^ 8j; 1 j m : ` (f ) i;0
PB006
i
i;j
148
Výsledkem výpoˇctu je množina substitucí.
M[ p℄ = ; M[ p℄ = f?g Pˇríklad:
:::::: ::::::
„No.“ „Yes.“
ˇ Ze sbírky hádanek pro chytré deti:
Jeden pes zje za jednu hodinu jednu kost’. Kol’ko psov zje za kol’ko hodín kol’ko kostí? ˇ je množina substitucí za „kol’ko“, „kol’ko“ a „kol’ko“ Správnou odpovedí ˇ nebyly pˇríliš rychle hotovy). (zde nekoneˇcná, aby s ní deti
Logické jazyky s (positivními) Hornovými klausulemi implicitneˇ pˇredpokládají úplnost teorie (tj. nelze-li dotaz z teorie odvodit, pak je „No“) – tzv. „closed world assumption“.
PB006
149
ˇ Rízení výpoˇctu ˇ Ve vetšin eˇ logických jazyku˚ záleží na poˇradí klausulí a na poˇradí podcílu˚ v klausuli (prostor substitucí se prohledává systematicky, takže i když ˇrešení existuje, nemusí se pˇri nevhodném poˇradí klausulí najít, anebo když ˇrešení neexistuje, nemusí se to v koneˇcném cˇ ase zjistit).
!
ˇ Operátor (ˇrez) v Prologu je ˇrídicím operátorem, který zabranuje opakovanému ˇ vyhodnocování podcíle, jestliže tento pocíl již jednou uspel.
f0 :- f1 ; !; f2 : ˇ a f2 následneˇ neuspeje, ˇ nehledá se už další úspešná ˇ Pokud f1 uspeje substituce
pro f1 .
f0 :- !:
Pokud se najde unifikátor pro f0 , nezkouší se s cílem unifikovat jiná klausule. PB006
150
Gödel
MODULE GCD. IMPORT Integers. PREDICATE G d : Integer * Integer * Integer. G d(i,j,d)
d). PREDICATE CommonDivisor : Integer * Integer * Integer. CommonDivisor(i,j,d)
151
Logické jazyky Prolog
70. léta, Marseille, Edinburgh netypovaný jazyk plochá struktura a viditelnost: – všechny predikáty jsou globální ˇ – všechny promenné jsou lokální (v klauzuli)
není cˇ isteˇ logický ˇ logický jazyk (napˇr. na FI Sicstus Prolog) nejrozšíˇrenejší PB006
152
Gödel
90. léta, Bristol (J. W. Lloyd) typovaný jazyk modulární struktura parametrický polymorfismus P. M. Hill, J. W. Lloyd : The Gödel Programming Language, MIT Press 1994 Mercury
multiparadigmatický jazyk (logický + funkcionální) polovina 90. let http://www. s.mu.oz.au/resear h/mer ury/ PB006
153
Aplikace logického programování
zpracování pˇrirozeného jazyka expertní systémy symbolická manipulace s výrazy, ˇrešení rovnic simulace Výhody
vyšší úroven,ˇ tj. program je bližší popisu problému než implementaci ˇ logika programu oddelena od ˇrízení výpoˇctu snazší dukazy ˚ korektnosti
Nevýhody
efektivita nevýhodné pro aplikace s intenzivním I/O
PB006
154
Funkcionální paradigma Patˇrí k deklarativním paradigmatum. ˚ Deklarativní paradigmata — funkcionální, logické, . . . ˇ Imperativní paradigmata — procedurální, objektové, soubežné, ...
PB006
155
Rysy funkcionálních jazyku˚
Nerozlišuje stavy, výpoˇcet je jednostavový )
nemá selektory složek stavu,
ˇ tj. pˇrepisovatelné promenné.
jazyky vycházejí z lambda kalkulu nebo kombinátorového kalkulu, tedy pracují pˇredevším s funkcemi a funkce jsou hodnotami „první kategorie“ ) vysoká míra ortogonality.
bohatý typový systém – parametrický polymorfismus, typové a konstruktorové tˇrídy uživatelské typy definice podle vzoru funkce vyššího ˇrádu, kombinátory líné vyhodnocování, nekoneˇcné datové struktury PB006
156
Sémantika funkcionálního jazyka Nepracuje se se stavy. Hodnotový kontext (prostˇredí)
Env
...
...
! Val
množina všech hodnotových kontextu˚
Sémantická funkce
Val
" : Var
M : Term Env ! Val
sémantická doména v netypovaných jazycích tvoˇrí jeden CPO (complete partial order) v typovaných jazycích systém CPO
CPO – jazyková katachréze, algebraická realita. PB006
:-) 157
CPO ˇ je uspoˇrádaná množina, v níž má každý nejvýše spoˇcetný ˇretezec supremum. monotónní funkce
f je monotónní, práveˇ když pro každé dva prvky x, y takové, že x v y, platí f (x) v f (y )
spojité funkce ˇ f jeG spojitá, práveˇ když každý spoˇcetný ˇretezec x 1 ; x2 ; : : : pro G f (x1 ; x2 ; : : :) = (f (x1 ); f (x2 ); : : :)
platí
Každá spojitá funkce je monotónní.
PB006
158
Sémantické domény Primitivní, tzv. ploché: Unit, Bool, Nat, Integer, Char Operace nad doménami Lift _ _ _ _
PB006
_ +_
!_
pˇridání nejmenšího prvku
?
kartézský souˇcin disjunktní sjednocení mocnina (doména spojitých funkcí)
159
Uspoˇrádání na doménách
8x 2 Lift D : ? v x 8x; y 2 D : (x v y , x v y) 8x ; y 2 D 8x ; y 2 D : (x v 1 y ^ x v 2 y , (x ; x ) v 1 2 (y ; y )) 8x ; y 2 D 8x ; y 2 D : ((x v 1 y , x v 1 2 y ) ^ (x v 2 y , x v 8f; g 2 D ! D : (f v 1! 2 g , 8x 2 D : f (x) v 2 g(x)) Lift D
Lift D
D
1
1
1
2
1
1
1
1
2
PB006
2
2
D
2
2
1
D
1
1
2
D
2
1
2
D
1
D
2
2
1
1
D
D
D +D
1
2
1
D
2
2
D1 +D2
y2 ))
D
160
Unit
()
()
Unit?
= Lift Unit
?
ff
tt
?
Bool?
0
Nat? PB006
1
?
2
3
...
... 161
(ff,())
(tt,())
(?,())
(ff,?)
(
Lift Bool?
Unit? )
(tt,?)
(?,?)
? () () ()
()
?
Bool?
PB006
! Unit?
?
?
()
()
()
?
?
? ? ? 162
ff ff ff
ff
ff
Bool?
ff
ff
?
?
?
?
tt tt tt
?
tt
?
tt
?
?
ff
ff
?
tt
tt
tt
?
?
tt
?
! Bool? ? ? ?
PB006
163
Sémantika konstant nezávisí na hodnotovém kontextu ". Pro libovolné "
2 Env
M[ True℄ " = tt M[ False℄ " = M[ 0 ℄ " = 0 .. .
PB006
M[ succ ℄ " : Val ! Val ; : : : M[ iszero℄ " : : : M[ not ℄ " : : : .. .
164
Sémantika výrazu˚
M[ x℄ " = "(x) M[ f e℄ " = 8 (M[ f ℄ ")(M[ e℄ ") [líná aplikace] < ?; když M[ e℄ " = ? M[ g e℄ " = : [striktní aplikace] (M[ g℄ ")(M[ e℄ ") jinak M[ x: e℄ " = f taková funkce z Val ! Val ; že 8t 2 Val : f (t) = M[ e℄ ("[x 7! t℄) PB006
165
8 > > > <
M[ e0 ℄ "; když M[ e℄ " = tt M[ if e then e0 else e00℄ " = > M[ e00℄ "; když M[ e℄ " = > > : ? jinak
PB006
166
Sémantika nerekursivních definic
M[ let v = e
1
in e
℄ " = M[ (v: e) e1 ℄ " = M[ e℄ ("[v 7! M[ e1 ℄ "℄)
M[ let v = e ; : : : ; v = e in e℄ " = M[ (v v : : : v : e) e e : : : e ℄ " = M[ e℄ ("[v 7! M[ e ℄ "; : : : ; v 7! M[ e ℄ "℄) 1
1
1
2
1
PB006
n
n
1
n
1
2
n
n
n
167
Sémantika rekursivních definic Pro funkcionální jazyk s líným vyhodnocováním lze sémantiku rekursivních definic zavést takto:
M[ letrec v = e ; : : : ; v = e in e℄ " = M[ e℄ "0 G 0 kde " = " , " = "[v 7! ?; : : : ; v 7! ?℄ 1
j
0
a pro každé j
PB006
j
0
0 je "
1
1
j +1
n
n
n
= " [v1 7! M[ e1 ℄ " ; : : : ; v 7! M[ e ℄ " ℄. j
j
n
n
j
168
Pˇríklad
M[ letrec f = n: if n == 0 then 1 else n f (n 1) in f ℄ " = M[ f ℄ "0 *
"0 "1 "2 "3 "4
= = = = = .. .
[f 7! f0 ℄ [f 7! f1 ℄ [f 7! f2 ℄ [f 7! f3 ℄ [f 7! f4 ℄
"0 = [f PB006
f0 f1 f2 f3 f4 .. .
G
? ? ? ? ? ?
0
0 1 2 3 4 :::
? ? ? ? 1 ? ? ? 1 1 ? ? 1 1 2 ?
? ? ? ? 1 1 2 6 ?
::: ::: ::: ::: :::
7! f ℄ j
169
Poznámka Sémantiku rekursivních definic dostaneme zadarmo, zavedeme-li tzv. kombinátor pevného bodu Y. Potom lze rekursivní definici v pro nerekursivní definici v
= Y(v: e).
= e považovat za syntaktickou zkratku
Potom
M[ letrec v = e in e℄ " = M[ let v = Y(v: e ) in e℄ " = M[ (v: e)(Y(v: e ))℄℄". G f (?), (kde Y = M[ Y℄ ", pro libovolné "), Platí Y f = 1
1
1
k
tedy Y
k
0
(v: e) = : : : ((v: e)((v: e)((v: e)((v: e)((v: e)?))))) : : : .
Pomocí kombinátoru pevného bodu se sémantika rekursivních definic zavádí také u jazyku˚ se striktním vyhodnocováním.
PB006
170
Funkcionální jazyky LISP (LISt Processing) – John McCarthy, konec 50. let jednoduchá syntax, stejná pro data i algoritmy – homoikonický jazyk není cˇ isteˇ funkcionální netypovaný dynamická viditelnost dialekty: AutoLisp, eLisp, . . . Scheme netypovaný jazyk vycházející z Lispu, 80. léta syntax podobná Lispu; statická viditelnost, striktní vyhodnocování, streamy ML typovaný jazyk, konec 70. let, Edinburgh striktní vyhodnocování dialekty: CaML, OCaML PB006
171
Erlang dynamicky typovaný jazyk se striktním vyhodnocováním konstrukce pro podporu paralelního vyhodnocování ˇ líneˇ vyhodnocované Hope, Clean, Orwell, Miranda konec 80. let, vesmes cˇ asto používané ve výuce programování; cˇ isteˇ funkcionální Opal 90. léta, cˇ isteˇ funkcionální, modulární, striktneˇ vyhodnocovaný Haskell cˇ isteˇ funkcionální, modulární, líneˇ vyhodnocovaný ˇ imperativních konstrukcí do referenˇcneˇ transparentního jazyka cˇ isté zaˇclenení pomocí monadických typu˚ a operací Cayenne, Agda, Epigram experimentální jazyky velmi silný (tedy nerozhodnutelný) typový systém
PB006
172
ˇ Soubežné zpracování ˇ Multitasking soubežné zpracování úloh na jednom poˇcítaˇci – úlohy využívají ruzné ˚ prostˇredky (typicky pomalejší I/O zaˇrízení) – interleaving – víceuživatelský režim ˇ je pˇrizpusoben ˇ – systém správy pameti ˚ soubežnému zpracování více úloh (stránkování, swapping, . . . ) ˇ Distribuované zpracování rozdelení úlohy na nezávislé podúlohy, méneˇ komunikace – výpoˇcetní shluky – globálneˇ distribuované úlohy ˇ ˇ Mobilní výpocty stehování výpoˇctu po síti
PB006
173
Víceprocesorové poˇcítaˇce ˇ nekolikaprocesorové (MIMD) mnohaprocesorové (teoretický model PRAM) procesorová pole (SIMD)
PB006
174
Interference a nezávislost Procesy P , Q jsou nezávislé, když jejich paralelní kompozice P
ˇ eˇ jjQ je vnejšn
deterministická. V opaˇcném pˇrípadeˇ jde o procesy interferující. Nezávislost procesu˚ je obecneˇ nerozhodnutelná. ˇ k nimž pˇristupují procesy P , Dostateˇcná podmínka nezávislosti: Jsou-li oblasti pameti,
ˇ procesy jsou také Q, disjunktní, a množiny dalších prostˇredku˚ využívaných obema disjunktní, jsou procesy nezávislé. Pˇríklad interferujících procesu: ˚
{ v := 1 ;
v := v + 1 }
jj
{ v := 0 ;
v := 3 v }
ˇ Existuje 6 možných prolínání, každé s jinou finální hodnotou promenné v: 0, 1, 2, 3, 4, 6.
PB006
175
Sémantiku paralelní kompozice interferujících procesu˚ nelze popsat pˇrímo pomocí sémantik jednotlivých procesu˚ (sémantika paralelní kompozice není skladebná). Pˇríklad: Necht’ je libovolný stav a oznaˇcme:
P1 = {i := 1}, P2 = {i := 2}, P10 = {i := 0 ; i := i + 1}, k = [i 7! k℄. Platí
ale
Tedy
PB006
[ P1 ℄ = [ P10 ℄ = f1 g [ P1 jj P2 ℄ = f1 ; 2 g [ P10 jj P2 ℄ = f1 ; 2 ; 3 g [ P1 jj P2 ℄ 6= [ P10 jj P2 ℄ 176
Naopak pro nezávislé procesy P , Q a každý stav platí jednoduše
[ P jj Q℄ = f[ ; ℄ j 2 [ P ℄ ; 2 [ Q℄ g
PB006
177
Od procesu˚ se obvykle oˇcekává, že budou kooperovat, tedy nemohou být nezávislé. Neˇrízená (živelná) interference je však nepraktická, protože neomezeneˇ interferující ˇ procesy je extrémneˇ težké programovat, ladit a spravovat. (Muže ˚ však mít smysl na hardwarové úrovni.) Proto je vhodné interferenci omezit na pˇresneˇ urˇcená místa výpoˇctu a oblasti sdílené ˇ pameti.
PB006
178
ˇ Podmínená kritická sekce ˇ Pˇrepisovatelné promenné sdílené procesy musí být jako takové deklarovány (shared var v ). Složený pˇríkaz region v do P vymezuje kritickou sekci vzhledem ke
ˇ v. Proces v kritické sekci muže ˚ být pozastaven (a pˇrístup ke sdílené sdílené promenné ˇ ˇ na základeˇ tzv. await podmínek. promenné uvolnen)
type MessageBuffer = record size, front, rear : 0..capacity ; items : array 1..capacity of Mes end; shared var buffer : MessageBuffer;
PB006
179
procedure sendmes (newitem : Mes); begin region buffer do begin await buffer.size
< capacity ;
:= buffer.size + 1; buffer.rear := buffer.rear mod capacity + 1; buffer.items[buffer.rear ℄ := newitem buffer.size
end end; procedure receivemes (out olditem : Mes); begin region buffer do begin await buffer.size
> 0;
:= buffer.size 1; olditem := buffer.items[buffer.front ℄; buffer.front := buffer.front mod capacity + 1 buffer.size
end end PB006
180
Semafory Semafor je globální objekt pˇrístupný pouze pomocí metod
(s; k) semwait (s) semsignal (s)
seminit
Skládá se ze tˇrí cˇ íselných hodnot:
(s; i) w . . . poˇcet provedených operací semwait (s) s . . . poˇcet provedených operací semsignal (s) Invariant: 0 w s + i. i
PB006
. . . iniciální hodnota zadaná operací seminit
181
Parent:
( 0); seminit (nonfull ; k ) seminit nonempty ;
Sender :
(
semwait nonfull
);
; semsignal (nonempty ) send_data
Receiver :
(
semwait nonempty receive_data
(
;
semsignal nonfull PB006
);
) 182
ˇ Problémy soubežného zpracování ˇ ˇ míˇre než pˇri Nedeterminismus – pˇri soubežném zpracování v mnohem vetší ˇ e) ˇ deterministické – chyby sekvenˇcním; cílem je psát programy globálneˇ (vnejšn ˇ výpoˇctu jsou vzniklé porušením tohoto pravidla se obtížneˇ detekují, protože behy prakticky neopakovatelné.
Závislost na relativní rychlosti zpracování. Zablokování – cˇ ekání procesu˚ na sebe navzájem. Zmítání – „živá“ varianta zablokování (procesy tráví cˇ as marnými pokusy na ˇ zablokování). odstranení ˇ Strádání – situace, kdy nekteré procesy „stojí“ (setrvávají ve stejném stavu) a ˇ na jejich úkor – je dusledkem ostatní beží ˚ tzv. nespravedlivého plánování.
PB006
183
progress of process 1
requires
R S
S held by
held by
1
requires
1
infeasible region R unsafe region
Deadlock
?
resource R
resource S
PB006
progress of process 2
184
Zablokování (deadlock) je stav, kdy množina procesu˚ cˇ eká na pˇrístup k prostˇredkum ˚ a z duvodu ˚ vzájemneˇ nekompatibilních požadavku˚ tento pˇrístup nezíská. K zablokování muže ˚ dojít, práveˇ když platí souˇcasneˇ následující podmínky: ˇ Vzájemné vylouˇcení – každý prostˇredek je pˇridelen nejvýše jednomu procesu. ˇ „Wait & hold“ – procesy cˇ ekající na prostˇredky si drží jiné dˇríve pˇridelené prostˇredky. Cyklické cˇ ekání – v bipartitním grafu procesu˚ a prostˇredku˚ s hranami „chce“ a „je ˇ pˇridelen“ je cyklus.
PB006
185
ˇ Rešení zablokování Neˇrešení – ignorování deadlocku až do zmrznutí OS, pak reboot. Detekce a zotavení – rozpoznání, že došlo k deadlocku, a zabití procesu. Prevence zrušením podmínky „wait & hold“ – vyžaduje se, aby každý proces požádal naráz o všechny prostˇredky, které bude potˇrebovat – plýtvání prostˇredky. ˇ Prevence zrušením podmínky cyklického cekání – na prostˇredcích se zavede lineární uspoˇrádání a vyžaduje se, aby byly požadovány jen v tomto poˇradí. Vyhýbání se zablokování – sledováním, zda se výpoˇcet nepˇriblížil nebezpeˇcné oblasti.
PB006
186
„Živá“ varianta deadlocku – livelock (zmítání). ˇ Algoritmus plánování pˇridelování prostˇredku˚ procesum ˚ je spravedlivý, když zaruˇcuje, že každý proces bude cˇ ekat na pˇrístup k požadovaným prostˇredkum ˚ nejvýše koneˇcneˇ dlouho.
PB006
187
