Тезисы докладов

информационные технологии

Программа, на которой проверяются выразительные возможности методов спецификации и верификации должна обладать двумя свойствами. С одной стороны, алгоритм, реализованный программой, должен быть достаточно сложным. С другой стороны, программа и ее аннотации должны быть сравнительно небольшими по объему, чтобы имелась возможность вручную применить методы и посмотреть результаты.

Эти свойства выполнены для таких олимпиадных задач по программированию, которые не только показывают оригинальность подхода к решению, но и требуют существенных усилий для строгого формального обоснования найденного решения. Программа проверки списка на зацикливание за линейное время является примером такой программы.

На примере этой программы, реализованной на языке C, показаны выразительные возможности следующих методов верификации, разработанных в проекте СПЕКТР:

1. метод описания операционной семантики языка C,

2. метод описания аксиоматической семантики языка C,

3. метод работы с указателями,

4. метод аннотирования программы,

5. метод доказательства частичной корректности,

6. метод доказательства завершимости,

7. метод доказательства условий корректности.

Примечание. Тезисы докладов публикуются в авторской редакции

Ваши коментарии Обратная связь

[Головная страница] [Конференции]

© 1996-2001, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2001, Сибирское отделение Российской академии наук, Новосибирск