契約プログラミングについて事後条件と不変条件がよくわかりません。

Question

契約プログラミングについてですが、事前条件についてはわかりましたが、残りの二つについてあまり理解ができません。
例えば以下の簡単なFunctionにて事前条件の違反となれば、二つの引数を想定しているのに対して一つだけやまたはタイプの違うstringを渡してもErrorで帰ってきます。これを事前条件の違反というのはsimpleで分かりやすいですが、事後条件と不変条件はwikipediaで見ても難しい言葉で説明してあってあんまりイメージがわきません。
大変初歩的な質問ではあると思いますが残り二つの違反とはどういうものなのか書きの簡単なFunctionを例に説明していただければと思います。

事後条件 (postcondition)

サブルーチンが、終了時に保証すべき性質。
不変条件 (invariant)
クラスなどのオブジェクトがその外部に公開しているすべての操作の開始時と終了時に保証されるべき、オブジェクト毎に共通した性質。
コードを呼ぶ側が事前条件と不変条件を満たす義務を負うことで、呼ばれたコードはその条件が恒真であるとの前提を利益として得る。引き換えに、呼ばれたコードは事後条件と不変条件を義務として負い、呼ぶ側の利益としてこれを保証する。...wikipediaより

def add_cal(a,b):
    sum = a + b
    print(sum)

add_cal(3)

Answer 1

【事後条件】

事前条件がインプットに対する違反チェックだとすれば、事後条件はアウトプットに対する違反チェックだと考えると分かりやすいと思います。

提示していただいたコードを例にすると、アウトプットは「a と b の和」になる想定ですが、以下のコードのアプトプットは「a と b の差」となっているので、事後条件の違反となります。

def add_cal(a,b):
    sum = a - b
    print(sum)

add_cal(5,3)

---

【不変条件】

不変条件は、この関数を実行するにあたって必要な「前提となる機能やデータ」の違反チェックです。

以下のコードで言うと、+ 演算子は「数値の和を求める機能」が求められますし、print 関数は「標準出力へ数値を出力する機能」が求められます。

def add_cal(a,b):
    sum = a + b
    print(sum)

add_cal(5,3)

この例では、ちょっと分かりづらいかもしれませんので、以下のURLも参考にしてみてください。

契約による設計から見た例外 - Qiita
https://qiita.com/Kokudori/items/2e4bd32abf7abea3186f

3-5. Javaのアサーション
https://www.ipa.go.jp/security/awareness/vendor/programmingv1/a03_05.html