Jednoczące teorie programowania

Unifying Theories of Programming ( UTP ) w informatyce zajmuje się semantyką programów . Pokazuje, w jaki sposób semantykę denotacyjną , semantykę operacyjną i semantykę algebraiczną w jednolite ramy formalnej specyfikacji , projektowania i wdrażania programów i systemów komputerowych .

Książka pod tym tytułem, napisana przez CAR Hoare i He Jifenga, została opublikowana w Prentice Hall International Series in Computer Science w 1998 roku i jest obecnie dostępna bezpłatnie w Internecie.

teorie

Podstawą semantyczną UTP jest rachunek predykatów pierwszego rzędu , uzupełniony o konstrukcje punktu stałego z logiki drugiego rzędu. Zgodnie z tradycją Erica Hehnera programy są predykatami w UTP i nie ma rozróżnienia między programami a specyfikacjami na poziomie semantycznym . Słowami Hoare'a :

Program komputerowy jest identyfikowany z najsilniejszym predykatem opisującym każdą istotną obserwację, jaką można poczynić na temat zachowania komputera wykonującego ten program.

W żargonie UTP teoria jest modelem określonego paradygmatu programowania. Teoria UTP składa się z trzech składników:

alfabet , który jest zbiorem nazw zmiennych oznaczających atrybuty paradygmatu, które mogą być obserwowane przez podmiot zewnętrzny ;
podpis , który jest zbiorem konstrukcji języka programowania nieodłącznym dla paradygmatu ; I
zbiór warunków zdrowotnych , które określają przestrzeń programów mieszczących się w paradygmacie. Te warunki kondycji są zwykle wyrażane jako monotoniczne idempotentne transformatory predykatów .

Udoskonalenie programu jest ważną koncepcją w UTP. Program jest udoskonalany przez ${\ displaystyle P_ {2}$ $} wtedy i tylko wtedy$ gdy każda obserwacja, której można dokonać, również obserwacją ${\ displaystyle P_ {2}}$ P. $\ Displaystyle P_ {1}}$ . Definicja udoskonalenia jest wspólna dla teorii UTP:

${\ Displaystyle P_ {1} \ sqsubseteq P_ {2} \ quad {\ tekst {jeśli i tylko wtedy}} \ quad \ lewo [P_ {2} \strzałka w prawo P_{1}\right]}$

gdzie $.$ uniwersalne zmiennych w alfabecie

Relacje

Najbardziej podstawową teorią UTP jest alfabetyczny rachunek predykatów, który nie ma ograniczeń alfabetycznych ani warunków zdrowotnych. Teoria relacji jest nieco bardziej wyspecjalizowana, gdyż alfabet relacji może składać się tylko z:

zmienne nieozdobione ( $,$ modelujące obserwację programu na początku jego wykonywania; I
zmienne primowane ( $) , modelujące$ programu na późniejszym etapie jego wykonywania

Niektóre wspólne konstrukcje językowe można zdefiniować w teorii relacji w następujący sposób:

Instrukcja skip, która w żaden sposób nie zmienia stanu programu, jest modelowana jako tożsamość relacyjna:

${\ Displaystyle \ mathbf {pomiń} \ równoważnik v '= v}$

Przypisanie wartości $}$ $E$ jest modelowane jako ustawienie $\ displaystyle$ mi $}$ i zachowanie wszystkich innych zmiennych (oznaczonych przez $u}$ $displaystyle a$ ) stała:

${\ Displaystyle a: = E \ równoważnik a' = E \ ziemia u' = u}$

Sekwencyjna kompozycja dwóch programów to po prostu relacyjna kompozycja stanu pośredniego:

${\ Displaystyle P_ {1}; P_ {2} \ równoważnik \ istnieje v_ {0} \ punktor P_ {1} [v_ {0}/v']\kraj P_{2}[v_{0}/v]}$

Niedeterministyczny wybór między programami jest ich największą dolną granicą:

${\ Displaystyle P_ {1} \ sqcap P_ {2} \ równoważnik P_ {1} \ lor P_ {2}}$

Warunkowy wybór między programami jest zapisywany przy użyciu notacji wrostkowej:

$\ Displaystyle P_ {1} \ trójkąt w lewo C \ trójkąt w prawo P_ {2} \ równoważnik (C \ ziemia P_ {1}) \ lor (\lnot C\land P_{2})}$

Semantyka rekurencji jest określona przez $fa$ ustalony punkt monotonicznego transformatora predykatu : ${F}}$ :

${\ Displaystyle \ mu X \ punktor \ mathbf {F} (X) \ równoważnik \ sqcap \ lewo \ {X \ mid \ mathbf {F } (X)\sqsubseteq X\right\}}$

Dalsza lektura

Woodcock, Jim ; Cavalcanti, Ana (2004). „Samouczek wprowadzenie do projektów w Unifying Theories of Programming” (PDF) . Zintegrowane metody formalne . Notatki z wykładów z informatyki , strony. Tom. 2999. Wiśniewski. s. 40–66. doi : 10.1007/978-3-540-24756-2_4 . ISBN 978-3-540-21377-2 .
Cavalcanti, Ana; Woodcock, Jim (2006). „Samouczek wprowadzenie do CSP w ujednolicaniu teorii programowania” (PDF) . Techniki udoskonalania w inżynierii oprogramowania . Notatki z wykładów z informatyki. Tom. 3167. Zygmunt. s. 220–268. doi : 10.1007/11889229_6 . ISBN 978-3-540-46253-8 .

Linki zewnętrzne