int foo()
{
  return 2000000000;
}

...

int i = foo();
int j = Int32.Parse(Console.ReadLine());

// i = i + j;  // тут анализатор предупреждает об опасности
// поэтому ставим иф
if (j < 100000)
  i = i + j;
else
  ...

int foo()
{
  return Int32.MaxValue - 1;
}

...

int i = foo();
int j = Int32.Parse(Console.ReadLine());

if (j < 100000)
  i = i + j;  // опять наш код сломался, нужен уже более сильный иф
else
  ...

T foo(U parameter) where T : Integer, U : Integer, T > U

        void A()
        {
            B("");
        }
        void B(string s)
        {
            C(s, 123);
        }
        void C(string s, int p)
        {
            Contract.NotNullOrEmpty(s);
            Contract.Ensures(p>=0);
        }

    struct NaturalNumber
    {
        [ContractInvariantMethod]
        protected void ObjectInvariant()
        {
            Contract.Ensures(this.Value>=0);
        }
        // ...
    }

fn search {n,m:nat | m <= n}
  (str : string n, sub : string m) : [p:int | p <= n - m] int p = ...

  def f(a:Int, b:Int) = {        //у нас есть функция и мы знаем (каким-то образом) что всегда 'a' = 800..1000, 'b' = 800, потому для них нужно по 2 байта;
    val c = a - b                //здесь мы можем вычислить что всегда 'c' = 0..200, следовательно для 'с' достаточно 1 байта;
    val d = c * 1000             //для 'd' уже нужно 3 байта;
    ...                          //и т.д.
  }

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging.

ARK>А что насчет переполнений?

int fun(int m, int n) {
    if (m == 0) {
        return n + 1;
    } else if (n == 0) {
        return fun(m-1, 1);
    } else {
        return fun(m-1, fun(m, n-1));
    }
}

object Test {
  def fun(m:Int, n:Int):Int = {
    if(m == 0){
      return n + 1}
    else if(n == 0){
      return fun(m-1, 1)}
    else{
      return fun(m-1, fun(m, n-1))}}              //> fun: (m: Int, n: Int)Int
      
  fun(4,4)                                        //> java.lang.StackOverflowError
                                              
}

   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);
}