Co-development of imperative programs and their correctness proofs in a type-theoretic environment
4РП — Обучение и мобилност на изследователи
- Период
- 1996-03-01 → 1998-02-28
- Финансиране от ЕС
- —
- Участници
- 2
- Схема
- RGI
Линиите свързват координатора с партньорите. За проекти отпреди 2014 г. CORDIS не винаги дава точни координати. Тези точки са на ниво град или държава.
Накратко на български
Теорията на типовете се изследва като основа за създаване на програми и формални доказателства за тяхната точност чрез системата LEGO. Това е важно, защото докато тестовете само намаляват грешките, математическото доказателство гарантира, че софтуерът работи според спецификацията.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Цел на проекта
In the last decade, outstanding progress in type theory has been achieved and sophisticated type-theoretic computer-aided proof assistants such as LEGO have been developed. The maturity of the LEGO system and its underlying expressive unifying theory of dependent types suggests that it is now feasible to apply the available tools to the problem of non-trivial formal program development. Often, it is insufficient to validate the correctness of a complex software system by relying merely on test data. Delivering the program together with a formal proof of its correctness with respect to some specification guarantees a correct program whereas tests can only reduce errors. Examples will be the driving force of this research. Focussing on imperative programming languages, the proposed research investigates type theory as a foundation for formal program development. Using the LEGO system, a framework for dealing with modularity and object orientation will be established.
Оригинален текст от CORDIS (на английски).
Участници
- UNIVERSITY OF EDINBURGH · EDINBURGHКоординаторОбединеното кралство
- Not availableНиво градГермания
Връзки
Данни: CORDIS, © Европейски съюз