Операции над высказывательными формами

Верификация программного обеспечения (2 часа)

Согласно стандарту СТБ ИСО 12207-2003 процесс верификации является процессом того, что программные продукты функционируют в полном соответствии с требованиями или условиями.

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

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

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

Исчисление высказываний

Исчисление высказываний - это совокупность правил для определения истинности или ложности высказываний.

Высказывание - это предложение, которое либо истинно, либо ложно.

Предложение “x²=4”, например, не является высказыванием, т.к. чтобы говорить об истинности или ложности высказывания, нужны дополнительные сведения (чему равно число x). В этом предложении x - некоторая переменная, вместо которой можно подставить элементы некоторого множества, называемые значениями этой переменной.

Предложение, которое содержит хотя бы одну переменную и становится высказыванием при подстановке вместо всех переменных их значений, называется высказывательной формой (ВФ).

В математической логике всякое предложение, составленное из высказываний с помощью логических связок (и; или; если то; тогда и только тогда, когда и т.п.), становится высказыванием.

Операции над высказываниями

1. Конъюнкция

2. Дизъюнкция

3. Отрицание

4. Импликация

Пример импликации:

Если будет хорошая погода, (А),

то я пойду в гости. (В), т.е.

Данное определение соответствует употреблению союза "если-то" не только в математике, но и в обыденной речи. По определению логической операции смысл составляющих высказываний не учитывается. Составляющие высказывания рассматриваются как объекты, обладающие единственным свойством: быть истинными или ложными.

Исчисление предикатов

Исчисление предикатов является расширением логики высказываний.

Рассмотрим высказывательную форму sin(x)=1. Данная форма каждому x на множестве действительных чисел ставит в соответствие некоторое высказывание и тем самым одно из значений истинности. Таким образом, данная высказывательная форма задаёт отображение множества действительных чисел R на множество значений {Истина, Ложь}, то есть задаёт функцию с областью определения R и множеством значений {ИСТИНА, ЛОЖЬ}.

Функция, все значения которой принадлежат множеству {ИСТИНА, ЛОЖЬ}, называется предикатом. Чаще всего предикаты задаются с помощью высказывательных форм.

Например,

- одноместная высказывательная форма,

- предикат с двумя неизвестными,

- трехместная высказывательная форма.

Операции над высказывательными формами

Конъюнкциейвысказывательных форм Ф₁ и Ф₂ называется высказывательная форма, истинная при тех и только при тех значениях входящих в неё переменных, которые обращают обе формы в истинное высказывание.

Дизъюнкциейвысказывательных форм Ф₁ и Ф₂ называется высказывательная форма, ложная при тех и только при тех значениях входящих в неё переменных, которые обращают обе формы в ложное высказывание.

Отрицаниемвысказывательной формы Ф называется высказывательная форма, ложная при тех наборах значений переменных, которые обращают высказывательную форму в истинное высказывание и наоборот.

Импликациейвысказывательных форм Ф₁ и Ф₂ называется высказывательная форма Ф₁ Ф₂, ложная при тех и только при тех значениях входящих в неё переменных, которые обращают Ф₁ в истинное высказывание, а Ф₂ - в ложное.