配列の合計のためのSpark-Adaの事後条件

Question

アレイの要素を合計する関数に対して、どのようにしてSpark事後条件を書いていますか？ （。スパーク2014、誰かが、私はそれを適応させることができる必要があり、以前のスパークのためにそれを行う方法を私に示している場合）

だから私は持っている場合：

type Positive_Array is array (Positive range <>) of Positive; 

function Array_Total(The_Array: Positive_Array) return Positive 
with 
    Post => Array_Total'Return = -- What goes here? 
is 
    -- and so on 

を私は心配する必要はありません。私の特定のケースではオーバーフローしています（私は総計が初期化されていることを知っており、単調に減少するだけです）。

おそらく、実装では証明者を助けるためにループバリアントが必要ですが、それは事後条件の簡単なバリエーションであるはずですので、まだ心配していません。

Answer 1

事後条件を書き込む1つの方法は、再帰関数として行うことができます。それは、実装と仕様の問題がまったく同じであることを避けるでしょう。