Oznacza to, że uzyskujemy możliwość dowodzenia faktów postaci: ten program jest poprawny względem warunku początkowego i warunku końcowego Formuła taka ma postać implikacji
Zastosowania AL w inżynierii oprogramowania możemy zapisywać specyfikacje oprogramowania i dokonywać weryfikacji poprzez dowody [], w projektowaniu języków programowania można opisać semantykę języka, podając odpowiednie aksjomaty i reguły wnioskowania, w opisie abstrakcyjnych struktur danych (co łączy się ze specyfikowaniem klas w językach programowania obiektowego) formuły algorytmiczne pozwalają w pełni scharakteryzować pewne struktury i klasy struktur.
Język określa się, podając jego alfabet i zbiór wyrażeń poprawnie zbudowanych WFF. W zbiorze wyrażeń poprawnie zbudowanych wyróżnia się trzy podzbiory: zbiór termów (albo zbiór wyrażeń nazwowych), zbiór formuł (zbiór wyrażeń logicznych) i zbiór programów (algorytmów).
Język logiki algorytmicznej jest konwolucją języka logiki pierwszego rzędu i języka programów.
Bibliografia
Kategoria:Algorytmika Kategoria:Logika matematyczna