Weryfikacja programów metodą logiki dynamicznej

• Autorzy: Zofia Łękawa

Warianty tytułu

Software Verification Using Dynamic Logic

• Języki publikacji: PL

Abstrakty

Dowód poprawności programu wymaga sformułowania odpowiednich własności (warunków) w odniesieniu do poszczególnych instrukcji Zadania tego nie można zmechanizować, gdyż wymaga ono zdolności i intuicji programisty. Nasuwa się więc pytanie o sens takiej weryfikacji programów.
Otóż z jednej strony jest rzeczą oczywistą, że chciałoby się mieć gwarancję, że program, który stosujemy (kupujemy), nie zawiera błędów. Z drugiej strony wiadomo, że duża część oprogramowania jest zawodna. Aby zwiększyć niezawodność programów, można postępować w dwojaki sposób. Można testować program na danych próbnych i w środowisku przetwarzania, a po względnie dużej liczbie wykonanych testów przyjąć, że program jest poprawny (jeśli oczywiście nie będzie błędów). Takie testowanie to inaczej szukanie błędów w programie. Zamiast jednak szukać błędów w programie, można udowodnić, że program jest poprawny, tak jak dowodzi się twierdzenia. W tym celu należy dokonać szczegółowej specyfikacji programu, a następnie przyjmując, że program będzie zrealizowany w skończonym czasie, wykazać niesprzeczność tej specyfikacji.
Wiele firm zajmujących się oprogramowaniem podaje, że około 50% nakładów związanych z budową oprogramowania przeznacza na testowanie programów. Stąd coraz większą rolę odgrywa weryfikacja programu. (fragment tekstu)

EN

The popular method of software verification is to test its correctness in the processing environment with sample data. It is assumed that a computer program is correct if there are no errors in it after a specified number of tests performed. Such proceedings are just the search for errors in software.
Instead, one can prove that a program is correct (just like a theorem is proved). To do this, it is necessary to give a detailed specification of a program and then, assuming that the program will be performed in a finite time, to prove the consistency of this specification. The method of dynamic logic has been applied to verify programs using a traditional framework of static mathematics for describing and explaining dynamic phenomena, in this case for describing a computer program. (original abstract)

Słowa kluczowe

PL

Logika; Analiza dynamiczna; Tworzenie oprogramowania; Testowanie oprogramowania

EN

Logic; Dynamic analysis; Software development; Software testing

• Czasopismo: Prace Naukowe Akademii Ekonomicznej we Wrocławiu. Informatyka i Ekonometria
• Rocznik: 1997
• Tom: 3
• Numer: nr 744 Zastosowania metod ilościowych
• Strony: 119--130

Twórcy

autor

Zofia Łękawa

Bibliografia

• Alagić S., Arabib M.A.: Projektowanie programów poprawnych i dobrze zbudowanych. Warszawa 1982.
• Banachowski L., Kreczmar A.: Elementy analizy algorytmów. Warszawa 1982.
• Blikle A.: An algebraic approach to mathematical theory of programs. ICS PAS Reports nr 119 Warszawa 1973.
• Blikle A.: A survey of input - output semantics and program verification. ICS PAS Reports nr З44. Warszawa 1979.
• Blikle A.: Notes on the mathematical semantics of programming languages. ICS PAS Reports nr 445. Warszawa 1981.
• Buchberger B.: Das Problem der Programmverifikation. Matematische Überblicke. Mannheim 1976.
• Hoare C.A.R., Wirth N.: An axiomatic definition of the programming language PASCAL. "Acta Informatica" 1973 nr 2.
• Liskov B.H., Zilles S.N.: Specification techniques for data abstractions. IEEE Transactions on Software Engineering 1975, SE-1, No. 1. (Tłum. ros. [w:] Dannye v jazykach programmirovanija. Abstrakcija i tipologija. Sbornik statej. Red. V.N. Agafonov. Moskva: Mir 1982).
• Łękawa Z.: Abstrakcyjne typy danych i ich zastosowania. Rozprawa doktorska. Akademia Ekonomiczna we Wrocławiu, 1994 (maszynopis).
• Ostasiewicz W.: Język PASCAL. Wrocław 1981 (maszynopis).