| Таблица | Карточка | RUSMARC | |
|
|
Разрешенные действия: –
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Группа: Анонимные пользователи Сеть: Интернет |
Аннотация
В данной работе изложен подход к доказательству корректности программ с помощью построения их денотационной семантики на основе определенной семантики операторов языка. Для этого рассмотрен и реализован язык охраняемых команд, предложенный Э. Дейкстрой в своем труде "Дисциплина программирования". Реализация языка состоит из интерпретатора программ и программного инструмента, выводящего предусловие программы по заданному постусловию. Язык снабжен средствами, позволяющими роектировать сложные алгоритмы методом пошагового уточнения. Рассмотрены примеры доказательства корректности некоторых лгоритмов с помощью этого инструмента. Язык охраняемых команд вместе с разработанными инструментами подходит как для построения корректных алгоритмов, так и для их публикации вместе с доказательством их корректности. Язык охраняемых команд хоть и является удобным для проведения формальных рассуждений, он не снимает с плеч программиста необходимости проектировать программный код, спецификацию программы и ее инварианты.
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.
Права на использование объекта хранения
| Место доступа | Группа пользователей | Действие | ||||
|---|---|---|---|---|---|---|
| Локальная сеть ИБК СПбПУ | Все |
|
||||
| Интернет | Авторизованные пользователи СПбПУ |
|
||||
|
Интернет | Анонимные пользователи |
Оглавление
- Эксперементы с реализацией языка охраняемых команд Дейкстры
- Введение
- 1. Денотационная семантика
- 2. Описание языка
- 3. Разработка интерпретатора и анализатора
- 4. Примеры программ
- Заключение
- Список использованных источников
- Приложение 1. Грамматическое описание языка
Статистика использования
|
|
Количество обращений: 11
За последние 30 дней: 0 Подробная статистика |