Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Coq

Sortuj według:

Ogranicz wyniki do:

Automation for Dependently Typed Functional Programming

Wilson S., Fleuriot J., Smaill A.

Fundamenta Informaticae

2010

Vol. 102, nr 2

209-228

Writing dependently typed functional programs that capture non-trivial program properties is difficult in current systems due to lack of proof automation. We identify proof patterns that occur when programming with dependent types and detail how automating such patterns allow us to work more comfortably with types that capture, for example, membership, ordering and nonlinear arithmetic properties. We describe the role of the rippling heuristic, both for inductive and non-inductive proofs, and generalisation in providing such automation. We then discuss an implementation of our ideas in Coq with practical examples of dependently typed programs, that capture useful program properties, which can be verified automatically. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined functions and inductive data types.

Wprowadzenie do weryfikacji prostych programów w języku ST za pomocą narzędzi Coq, Why i Caduceus

Sadolewski J.

Metody Informatyki Stosowanej

2009

nr 2 (19)

121-138

Przedstawiono metodę przeprowadzania dowodów poprawności prostych programów sterowania napisanych w języku ST w środowisku Coq. Wykorzystano w tym celu dwa pomocnicze narzędzia Why i Caduceus należące do wspólnego projektu Proval. Metoda polega na ręcznej konwersji programu sterowania zapisanego w języku ST za pomocą przedstawionych reguł do równoważnej postaci w ANSI C. Ze względu na prostotę ST i podobieństwo do ANSI C nie powinno stanowić to problemu. Postać tę uzupełnia się o specyfikację wejść i wyjść a następnie poddaje automatycznym transformacjom programami Caduceus i Why. Program Why generuje lematy, które należy udowodnić, aby wykazać poprawność realizacji. Przedstawione reguły konwersji z języka ST do ANSI C stosuje się do przekształcania prostych bloków funkcjonalnych i programów. Zastosowanie niektórych reguł prowadzi do ograniczeń w liczbie instancji bloków, co jest wadą zaproponowanego rozwiązania. Wśród pozytywnych cech prezentowanych reguł wyróżnić można przejrzysty zapis specyfikacji i łatwość przeprowadzania dowodów w podobnych przypadkach.

Based on three simple examples, the paper introduces into verification technique of control programs by means of Coq, Why and Caduceus tools developed in France. The examples involve binary multiplexer, RS fillip-flop and a Start-Stop circuit composed of theflip-flop and a gale. The programs to be verified are written in ST language (Structured Text) of lEC 61131-3 standard. The approach consists of four basic steps. First the original ST program is converted into ANSI C to be handled by Caduceus. This in turn converts the ANSI C into a code interpreted by Why. Coq is a proof assistant for verificaton of conditions generated by Why. Conversions and proofs for each of the examples are presented in details, together with trees involving tactics applied for verification. Based on these, some recommendations and hints how to handle problems of similar classes are given.