verifiable-c

3熱度

2回答

已驗證的軟件工具鏈：if-then-else proof

我正在學習使用Verified Software Toolchain（VST）。我被困在證明一個簡單的「if-then-else」塊。 這裏是.c文件： int iftest(int a){ int r=0; if(a==2){ r=0; else{ r=0; } return r; } 我寫一個關於iftest()如下規格：

coq verifiable-c 2013-08-20

---

0熱度

1回答

PLCC書。第23頁。這是一個錯字，應該西格馬替代西格瑪？

在編程邏輯的認證編譯器的書，對頁＃23，在表達： (v ≠ 0 ∧ ∃σ' ∃h∃t. σ = h · σ' ∧ v.head->h ∗ v.next->t ∗ listrep σ (t, 0)) 在我看來，是因爲σ表示整個列表v和σ」代表的尾巴，最後一個表達式應該是：listrep σ' (t, 0)。這是否正確，這只是書中的印刷錯誤？

verifiable-c 2015-01-12

---

0熱度

1回答

semax_func_cons - 沒有適用的策略

我想爲我的兩個功能樣張拼湊成一個證明了整整一個程序： ... Definition Vprog : varspecs := nil. Definition Gprog : funspecs := get_spec :: set_spec :: nil. Lemma body_get: semax_body Vprog Gprog f_get get_spec. Proof. ...

verifiable-c 2015-01-14

---

0熱度

1回答

帶本地變量的forward_call

VST版本1.7。 我有一個問題，當我嘗試在函數調用中使用它們時，coq將無法識別本地聲明的變量。我的代碼： void deSignArray(int bits[], int invKey, int size) { int i = 0; while (i < size) { int bit = bits[i]; int ans = deSignInt(bit, invKey); bit

coq verifiable-c 2016-11-12

---