| Table | Card | RUSMARC | |
|
|
Allowed Actions: –
Action 'Read' will be available if you login or access site from another network
Action 'Download' will be available if you login or access site from another network
Group: Anonymous Network: Internet |
Annotation
В данной работе изложен подход к доказательству корректности программ с помощью построения их денотационной семантики на основе определенной семантики операторов языка. Для этого рассмотрен и реализован язык охраняемых команд, предложенный Э. Дейкстрой в своем труде "Дисциплина программирования". Реализация языка состоит из интерпретатора программ и программного инструмента, выводящего предусловие программы по заданному постусловию. Язык снабжен средствами, позволяющими роектировать сложные алгоритмы методом пошагового уточнения. Рассмотрены примеры доказательства корректности некоторых лгоритмов с помощью этого инструмента. Язык охраняемых команд вместе с разработанными инструментами подходит как для построения корректных алгоритмов, так и для их публикации вместе с доказательством их корректности. Язык охраняемых команд хоть и является удобным для проведения формальных рассуждений, он не снимает с плеч программиста необходимости проектировать программный код, спецификацию программы и ее инварианты.
This work presents an approach to proving the correctness of programs by constructing ther denotational semantics based on defined semantics of language operators. To do this, there was considered and implemented the guarded command language, proposed by E. Dijkstra in his work "A discipline of programming". The implementation of the language consists of a interpreter and a software tool that derives program precondition for a given postcondition and invariants. The language is developed with tools that allow to design complex algorithms using the stepwise refinement method. Some examples of proving the correctness of algorithms are considered. The guarded command language, alongside with the developed tools, is suitable both for building correct algorithms and for publishing them alongside with their correctness proof. Although the guarded command language is convenient for conducting formal reasoning, it does not remove the need to designb the program specification, program code and it's invariants from the programmer shoulders.
Document access rights
| Network | User group | Action | ||||
|---|---|---|---|---|---|---|
| ILC SPbPU Local Network | All |
|
||||
| Internet | Authorized users SPbPU |
|
||||
|
Internet | Anonymous |
Table of Contents
- Эксперементы с реализацией языка охраняемых команд Дейкстры
- Введение
- 1. Денотационная семантика
- 2. Описание языка
- 3. Разработка интерпретатора и анализатора
- 4. Примеры программ
- Заключение
- Список использованных источников
- Приложение 1. Грамматическое описание языка
Usage statistics
|
|
Access count: 19
Last 30 days: 2 Detailed usage statistics |