Table of Contents
Úvod do paralelného programovania
Základné crty teórie, ktorú budeme pouzívat:
UNITY
Príklad: Urcenie termínu schôdzky
UNITY riešenia
UNITY riešenia 2
UNITY riešenia 3
UNITY Program Structure
UNITY Program Structure 2
UNITY Program Structure 3
UNITY Program Structure 4
UNITY Program Structure 5
UNITY Program Structure 6:Assign section
UNITY Program Structure 7:Initially section
UNITY Program Structure 8:Initially section, príklady
Sorting
Binomial Coefficients
UNITY Program Structure 9:Always section
UNITY Program Structure 10
Programming Logic
Dokazovanie tvrdení o priradovacích príkazoch
Kvantifikované tvrdenia
Výpoctový model
Základné pojmy
Unless
Špeciálne prípady unless (stable, invariant)
Ensures
Leads-to
Pevný bod
Theorems about unless
Theorems about unless 2
Theorems about unless 3
Theorems about ensures
Theorems about ensures 2
Theorems about leads-to
Theorems about leads-to 2
Theorems about leads-to 3
Theorems about leads-to 4
Indukcný princíp pre leads-to
Theorems about FP
Architektúry a zobrazenia, ASM
Architektúry a zobrazenia, DS
Architektúry a zobrazenia, SM
Architektúry a zobrazenia, SM 2
Read-only schéma
Shared-variable schéma
Ekvacionálna schéma
Jednopríkazová schéma
Výpocet maxima, SA
Výpocet maxima, PA
Výpocet maxima, PA 2
Najkratšia cesta
Najkratšia cesta 2: stratégia
Najkratšia cesta 3: stratégia
Najkratšia cesta 4
Najkratšia cesta, SA
Najkratšia cesta, SA 2
Najkratšia cesta, PSA
Najkratšia cesta, PSA 2
Najkratšia cesta, ASM
Najkratšia cesta, ASM 2
Najkratšia cesta, ASM 3
Porovnanie dvoch neklesajúcich postupností
Porovnanie dvoch neklesajúcich postupností 2
Porovnanie dvoch neklesajúcich postupností 3, PA
Dosiahnutelnost v orientovanom grafe G = (V, E)
Silmulácia Petriho sietí
Readers?Writers Problem
Readers?Writers Problem 2
Readers?Writers Problem 3
Readers?Writers Problem 4
Spojenie programov
Spojenie programov 2
Spojenie programov 3
Protokol na komunikáciucez chybové kanály (Faulty channels)
Faulty channels 2
Faulty channels 3
Faulty channels 4
Faulty channels 5
Faulty channels 6 ? Chybné kanály
Faulty channels 7 ? Safety vlastnosti
Faulty channels 8 ? Progress vlastnosti
Faulty channels 9 ? Program FC
Faulty channels 10 ? Protokol...
Faulty channels 11 ? ...a jeho správnost
Faulty channels 12 ? Optimalizácia
Global snapshots
Global snapshots 2
Global snapshots 3
Global snapshots 4
Global snapshots 5 ? Hlavná myšlienka
Global snapshots 6
Global snapshots 7
Global snapshots 8
Global snapshots 9
Global snapshots 10
Global snapshots 11
Vecerajúci filozofi
Vecerajúci filozofi 2
Vecerajúci filozofi 3
Vecerajúci filozofi: Spec1
Vecerajúci filozofi: Spec2
Vecerajúci filozofi: Spec2
Vecerajúci filozofi: Spec3
Vecerajúci filozofi: Spec4
Vecerajúci filozofi: Spec4
Vecerajúci filozofi: Spec5
Vecerajúci filozofi: Spec5
Vecerajúci filozofi: Program pre os
Byzantská dohoda
Byzantská dohoda: Spec1
Byzantská dohoda: Spec2
Byzantská dohoda: Spec2
Byzantská dohoda: Spec3
Byzantská dohoda: Spec3
Byzantská dohoda: Spec3
Byzantská dohoda: Spec4
Byzantská dohoda: Program
Triedenie
Triedenie
Triedenie ? Jednoduché riešenia
Triedenie ? Jednoduché riešenia
Triedenie ? Sekvencné architektúry
Triedenie ? Sekvencné architektúry
Triedenie ? Sekvencné architektúry
Triedenie ? Sekvencné architektúry
Triedenie ? Paralelné architektúry (synchrónne)
Triedenie ? Rank sort
Temporálne logiky
Lineárna temporálna logika
Propozicná lineárna temporálna logika
Branching temporálna logika
Propozicná branching temporálna logika
Propozicná branching temporálna logika
Deduktívne systémy
Deduktívne systémy 2
Model checking
Temporálne logiky ? obrázky
|