procedure Dedupe (Arr: in out Int_Array; Last : out Natural) with
     Pre => Has_Duplicates(Arr),
     Post => not Has_Duplicates( Arr(Arr'First .. Last) )
             and then (for all Item of Arr'Old =>
                        (for some J in Arr'First .. Last =>
                            Item = Arr(J)))
                      -- Only duplicates removed
             and then (for all J in Arr'First .. Last =>
                        (for some Item of Arr'Old =>
                            Item = Arr(J)));
                      -- Nothing new added

   function Has_Duplicates(Arr : Int_Array) return Boolean is
   begin
      return (for some I in Arr'First .. Arr'Last-1 =>
              (for some J in I+1 .. Arr'Last => Arr(I)=Arr(J)));
   end Has_Duplicates;

type Disc_Pt is
  record
    X, Y: Float range –1.0 .. +1.0;
  end record
  with
    Type_Invariant => Disc_Pt.X**2 + Disc_Pt.Y**2 <= 1.0;

P.X := 1.0;
P.Y := 0.0;

int SafeAdd(int val)
{
  return (val < Int32.MaxValue) ? (val + 1) : 0;
}

Устойчивость против корректности
Как нам показали примеры с видеоигрой и рентгеновской установкой, выбор подходящего
метода обработки ошибки зависит от приложения, в котором эта ошибка
происходит. Кроме того, обработка ошибок в общем случае может стремиться
либо к большей корректности, либо к большей устойчивости кода. Разработчики
привыкли применять эти термины неформально, но, строго говоря, эти термины
находятся на разных концах шкалы. Корректность предполагает, что нельзя
возвращать неточный результат; лучше не вернуть ничего, чем неточное значение.
Устойчивость требует всегда пытаться сделать что-то, что позволит программе
продолжить работу, даже если это приведет к частично неверным результатам.
Приложения, требовательные к безопасности, часто предпочитают корректность
устойчивости. Лучше не вернуть никакого результата, чем неправильный
результат. Радиационная машина — хороший пример применения такого принципа.
В потребительских приложениях устойчивость, напротив, предпочтительнее корректности.
Какой-то результат всегда лучше, чем прекращение работы. Текстовый
редактор, которым я пользуюсь, временами показывает последнюю на экране
строку лишь частично. Хочу ли я, чтобы при обнаружении этой ситуации
редактор завершал выполнение? Нет: когда я в следующий раз нажму Page Up или Page
Down, экран обновится, и изображение исправится.

ARK>В подавляющем большинстве случаев все-таки будет вариант B.

ARK>int SafeAdd(int val)
ARK>{
ARK>  return (val < Int32.MaxValue) ? (val + 1) : 0;
ARK>}
ARK>

int AddModU32(UInt32 a, UInt32 b)
{
  int max = UInt32.MaxValue - a;
  if (b <= max) {
    return a + b; // No overflow
  }

  return max - b; 
}

ARK>Но программа остается непонятно в каком состоянии. Босс продолжает битву, но становится неубиваемым.

M>А теперь можно думать, как это все разрулить

• Использовать пометку кода. На практике решение состоит в том, чтобы принудительно устанавливать некоторую опцию, а потом восстановить старое значение.
  
• Использовать специальные функции, благо их не много
  
• Использовать специальные типы

public int Mid(int a, int b)
{
  return (a + b)/2; // arrgh!
}

public int Mid(int a, int b)
{
  return (a * b)/2; // arrgh!
}

public uint Factorial(uint n)
{
  switch(n)
  {
    case 0:
    case 1: return 1
    default: return n*fac(n-1);
  }
}

ARK>Так вот, ИМХО, автоматический вывод контрактов совершенно не способствует созданию модульного, компонентного ПО. Если вообще не препятствует этому.

public void DoWork()
{
   Contract.GenerateContractByImplementation();// явное указание, что контракты нудно сгенерить
   
   DoWork(DefaultArg);
}