Где используется Обозначение Общее определение Примеры Множества Типы Условия Применение   Принцип LSP Изменение условий вывода при доказательстве правильности

 

---

Где используется

 

Понятия достаточно широкие, и соответственно могут использоваться как в математике, так и в физике, так и в computer science, так и при математическом доказательстве правильности программ (см. вики и wiki).

 

Обозначение

 

Если A ковариантен B, то это будем записывать как A cov B.

Если A контравариантен B, то это будем записывать как A contrav B.

Если A инвариантен B, то это будем записывать как A inv B.

 

Общее определение

 

A cov B тогда true, когда все что есть в B есть в A. Или более точно: условие A всегда захватывает B.

A contrav B тогда true, когда все что есть в A есть в B. Или более точно: условие B всегда захватывает A.

A inv B тогда true, когда все что есть в А есть в В, а также все что есть в B есть в A; или A cov B и при этом B cov A.

 

Примеры

 

Множества

 

{x,y,z} cov {x, y} = true

{x,y,z} cov {x, y, z} = true

{x,z} cov {x, y} = false

{x} cov {x, y} = false

{x} cov {} = true

{x} cov {x, y} = false

 

Типы

 

Пусть имеется иерархия наследования:

 

 

Здесь:

 

{инструмент} cov {отвертка} = true

{инструмент} cov {крестовая отвертка} = true

{инструмент} cov {отвертка; молоток} = true

{отвертка} cov {молоток} = false

{отвертка} cov {инструмент} = false

{отвертка;молоток} cov {инструмент} = false

 

Условия

 

{x > 0} cov {x > 1} = true

{x > 0} cov {false} = true

{x > 0} cov {true} = false

{x > 0} cov {x > 0 and y > 0} = true

{x > 0} cov {x > 0 or y > 0} = false

{x > 0 and y > 0} cov {x > 0} = false

{x > 0 and y > 0} cov {x > 1} = false

 

Применение  

 

Принцип LSP

 

Пусть имеется базовый тип A и его подтип B.

Для них необходимо, чтобы для любой функции

 

type1

func( type2 value );

 

выполнялось:

 

A::type1 cov B::type1

A::type2 contrav B::type2

 

Т.е. например можно так:

 

class A {
    float
    func( double x );
};
 
class B: public A {
    double
    func( float x );
};

 

Но нельзя так:

 

class A {
    float
    func( double x );
};
 
class B: public A {
    double
    func( float x );
};

 

Также для функции если существует любое предусловие pred и любое постусловие post, то необходимо, чтобы выполнялось 

 

A::pred contrav B::pred

A::post cov B::post

 

Например:

 

1. Имеется предусловие перед созданием объекта A о необходимости открытого файла f. Тогда в предусловии создания объекта B этот файл может быть как открыт, так и нет.
2. Имеется постусловие после выхода из полиморфной функции объекта A - внутренняя функция Release() должна быть вызвана. Соответственно, в этой же функции в объекте B внутренняя функция Release() также должна быть вызвана.

 

 

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

 

Если рассматривается программа в виде троек Хоара

 

{P} C {Q}

 

то при движении в прямом направлении можно усиливать условия. Т.е. должно выполнятся Q_old cov Q_new.

Соответственно при движении в обратном направлении должно выполняться  P_old contrav P_new.

 

Например имеем программу и предусловие:

 

{x > 0}
x = x + 1;

 

Для неё постусловие есть {x > 1}. Но чтобы сказать, что {x > 0} возможно будет достаточно доказательства что {x > 2}.

 

И для постусловия:

 

x = x + 1;
{x > 0}

 

Здесь предусловием будет {x > -1}. Но данное предусловие можно усилить. Т.е. если мы докажем, что {x > 0}, то это также будет доказывать, что {x > 0} после инкремента.