Ковариантность и контравиантность

Понятия достаточно широкие, и соответственно могут использоваться как в математике, так и в физике, так и в 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

См. 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} после инкремента.

Рафинирование