Введение утверждений в программные тексты

Введение утверждений в программные тексты

Как только корректность ПО определена как согласованность реализации с ее спецификацией, следует предпринять шаги по включению спецификации в сам программный продукт. Для большинства в программистском сообществе это все еще новая идея. Привычно писать программы, устанавливая тем самым, - как делать (the how); менее привычно рассматривать описание целей - что делать (the what) - как часть программного продукта.

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

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

Синтаксически утверждения в нашей нотации будут обычными булевыми выражениями с небольшими расширениями. Одним из расширений является введение в нотацию термина "old", другим - введение символа ";" для обозначения конъюнкции (логического И). Вот пример:

n>0; x /= Void

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

Positive: n > 0

Not_void: x /= Void

Метки, такие как Positive и Not_Void, в период выполнения играют роль утверждений, что будет еще обсуждаться в этой лекции. В данный момент они введены, главным образом, для ясности и документирования. В нескольких последующих разделах будет дан обзор принципиальных возможностей применения утверждений: как концептуального средства, позволяющего создавать корректные системы, и как документирование того, почему они корректны.

Поделитесь на страничке

Следующая глава >

Похожие главы из других книг:

Приложение 3 Исходные тексты калькулятора hoc

Из книги автора

Приложение 3 Исходные тексты калькулятора hoc These files contain all the code from "The Unix Programming Environment", by Brian Kernighan and Rob Pike (Prentice Hall, 1984, ISBN 0-13-937681-X). A separate hoc6 distribution contains any fixes that we have applied to that; the version in this file is from the book.Copyright © Lucent Technologies, 1997. All Rights ReservedPermission to use, copy, modify, and distribute this software and its documentation for


Вариант 1 – Автоматические тексты

Из книги автора

Вариант 1 – Автоматические тексты Есть полуавтоматические способы создания текстовой информации. Их плюс в том, что для Google и Яндекс они будут уникальными Это быстро и относительно недорого Здесь вы берете количеством. Минус – контент получится достаточно «мусорным» и


Продающие тексты для вашего сайта

Из книги автора

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


Как правильно писать тексты для поисковых систем

Из книги автора

Как правильно писать тексты для поисковых систем SEO-копирайтинг предполагает написание текстов с целью оптимизации поиска сайта. Статьи пишутся с использованием ключевых слов и призваны поднимать рейтинг сайта в поисковых системах (Google, Yandex, Rambler и др.).Естественно, сайт,


2.6.1. Успешное доказательство конъюнкции целевых утверждений

Из книги автора

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


1.5.4. Исходные тексты

Из книги автора

1.5.4. Исходные тексты Linux — система с открытым кодом, не так ли? Верховным судьей, определяющим, как работает система, является исходный код самой системы. К нашему счастью, он доступен бесплатно. В имеющийся дистрибутив Linux могут входить исходные тексты всей системы и всех


А.3.5. Исходные тексты программы-калькулятора

Из книги автора

А.3.5. Исходные тексты программы-калькулятора В листинге А.3 показан текст программы, вычисляющей значения постфиксных выражений.Листинг А.3. (calculator.c) Основная часть программы-калькулятора/* Вычисления в унарном формате. *//* На вход программы подаются однострочные


Использование утверждений

Из книги автора

Использование утверждений Теперь мы уже познакомились со всеми конструкциями, содержащими утверждения. Разумно, еще раз взглянуть на те преимущества, которые мы можем получить от этого. Выделим четыре основных применения.[x]. Помощь в создании корректного ПО.[x]. Поддержка


Мониторинг утверждений в период выполнения

Из книги автора

Мониторинг утверждений в период выполнения Пришло время, дать полный ответ на вопрос: "какой эффект производят утверждения в период выполнения?". Как отмечалось, ответ определяется разработчиком, имеющим возможность управлять параметрами компиляции. Выбор нужных


Выразительная сила утверждений

Из книги автора

Выразительная сила утверждений Как можно было заметить, применяемый язык утверждений является языком обычных булевых выражений, обогащенный несколькими понятиями, такими как old. Как результат, он ограничен и не позволяет включить в наши классы некоторые свойства,