b05902132 / formal Goto Github PK

b05902132 林敬文

本次project要證明merge sort，為了證明方便拆成兩個function，merge_sort跟merge，
放在不同檔案，這樣prover可以不用看到一些無關的敘述。
function的precondition跟postcondition都放在merge_sort.h。

證明時有使用到Coq，使用的script放在/coq_script中，檔名跟assertion的名字一致。
為了方便起見，這些script我也放在/.frama_c裡面，wp會自己到這個資料夾找coq的script。

證明時請使用-wp -wp-rte -wp-prover=coq,alt-ergo -wp-timeout=300，
而且請一次只證明一個檔案。
證明某些變數沒有改變時花的時間異常地久，請稍候。


Coq的證明大多有寫註解，難懂的證明會寫的比較詳細。
有些指令用到的地方比較多就統一列在這裡。

  lia可以用來自動證明有關整數的定理，在比較舊的Coq中稱為omega，
  需要Import才能用。

  natlike_ind顧名思義就是用來在整數上做自然數的數學歸納法，
  如果想證明的定理是0 <= z -> P z，則可以apply natlike_ind P。
  有的時候P會很長，看起來就會很醜，不過我找不到要怎麼自動化。
  （有時候apply natlike_ind可以自動偵測出P是啥，
    不過這次有用到的地方沒有一個是有辦法偵測出來的。)



證明進度：
   merge_sort完全證明完畢。
   
  merge的部分沒辦法證明只有Assign到Out，儘管函式內動到的變數只有這個不是Global
  ariable。

  merge還有另外一個無法證明的assertion，loop1_append_i1_loop2，證明這個需要用到
  記憶體的一些性質，超出我的能力範圍。(神奇的是證明另一個對應的迴圈卻不用。)

  

使用的工具版本：
why3 1.3.3
frama-c 22.0
coq 8.12.2
alt-ergo 2.3.3