Предикат H(x, y) является однозначным в области X для набора переменных x, если он определяет функцию, отображающую значения набора x в значения набора y. Должно быть истинным следующее условие:
"xÎX "y1,y2. H(x, y1) & H(x, y2) Þ y1 = y2 .
Отметим, что однозначный предикат в некоторой области X не обязательно является реализуемым в этой области.
Оператор S является однозначным в области X, если формула LS(S)(x, y) однозначна в области X. Нетрудно убедиться, что оператор суперпозиции A; B, параллельный оператор A || B и условный оператор if (C) A elseB являются однозначными, если однозначными являются операторы A и B.
Спецификация оператора S, представленная предусловием P(x) и постусловием Q(x, y), является однозначной, если постусловие является однозначным в области предусловия, т. е.
"x. P(x) Þ "y1,y2. (Q(x, y1) & Q(x, y2) Þ y1 = y2) .
Отметим, что однозначная спецификация не обязательно является реализуемой.
Лемма 2.7. Допустим, предикат D(x, y) является однозначным в области X, а предикат Z(x, y) реализуем в области X. Пусть истинна формула Z(x, y) Þ D(x, y). Тогда истинна следующая формула: "xÎX. D(x, y) Þ Z(x, y). Как следствие, предикаты D и Z оказываются тождественными в области X.
Доказательство. Пусть истинно D(x, y) для некоторого xÎX. Докажем истинность Z(x, y). Поскольку предикат Z реализуем, то существует некоторый y’, для которого истинно Z(x, y’). Из Z(x, y) Þ D(x, y) получаем истинность D(x, y’). Поскольку истинны D(x, y) и D(x, y’), то из однозначности D следует y = y’. Тогда истинно Z(x, y). □