下方示範對函式 sum
綁定事件 sum(a, b)
,在執行完最後一條敘述return s
後,將產生該事件,每當該函式被呼叫執行一次後,都會產生該事件。
在這個事件自動機中,自動機變數和事件的參數類型限制在整型 (int)、實數 (real) 和布林值 (bool)。
C 程式中也會保存字元串類型的變數,在綁定事件時,可以進行映射,也就是說,將字串型變數映射到整數型態。事件自動機變數不可以是指標型態,因為指標型態如果指向程式中的變數地址,會導致自動機轉移修改程序的變數,這在監視過程中是不允許的。
自動機理論 (automata theory) 探討運算的數學模型,包括相關的定義與特性,這些模型在很多電腦科學的應用領域中都扮演相當重要的角色。其中有限自動機 (finite automation)應用於 text processing, compiler 與硬體設計,與上下文無關的文法 (context-free grammar) 則運用於程式語言與人工智慧
自動機理論很適合當做運算理論的入門主題,因為運算性的理論與複雜度理論都需要電腦的精確定義,這在自動機理論中經常可以看到實際的例子
有限自動機 (finite automata) 可看成是一種模型,用來描述擁有極為有限的記憶體的電腦。在這麼少的記憶體的情況下,這種電腦能有什麼作用呢 ? 其實日常生活中有很多設備都具有類似的功能,例如下圖顯示的自動門,假如有人站在前感應區,則自動門應該開啟,即使行人通過前感應區,來到後感應區,自動門還是要開啟一下,讓行人有足夠的時間離開。
自動門的作用可用狀態圖 (state diagram) 來表示
上圖的狀態圖清楚地顯示出當什麼情況發生時,自動門的狀態會有什麼變化。控制自動門的設備就像是一種有限自動機,只有單一位元(bit)的記憶體。
延伸閱讀: 自動機理論
下圖示範一個描述檔案操作的事件自動機實例,有 3 個狀態:
當自動機接收到一個 open 事件後,就將 open 中的參數指派到自動機變數f
。顯然,自動機描述了所有打開一個檔案後,但是程式終止時卻沒有關閉檔案的執行路徑。
在狀態 s0 使用完全事件,好處在於當程式同時打開多個檔案時,可以只用這一個事件自動機進行表達。
.
,不要漏掉)Build files have been written to: /home/jserv/cbmc
的輸出訊息,就可以著手編譯:bin/
目錄見到 cbmc
一類的執行檔。複製到 $HOME/.local/bin
或者其他 $PATH
環境變數可找到的目錄sidneycadot/cbmc
取得示範的程式碼倘若 model checking 的條件更嚴格,像是追加 --bounds-check --pointer-check
參數,那 cbmc 會驗證失敗:
回頭閱讀 logic.c
,對照上述訊息,思考為什麼
verify
標的,可透過 cbmc 來驗證由 Ilya O. Levin 開發、獨立於 moxiebox 專案的 SHA256 實作runtime
目錄,執行 $ make verify
命令,參考輸出如下: (需要等待,請保持耐心)通過了 cbmc 以下條件:
修改 sha256_test.c
,將 Line #35 從原本的
將「小於」換成「小於等於」,如下:
重新執行 $ make verify
,得到不同的輸出訊息: