Coq中的狀態機

Question

我可以使用Coq來證明狀態機無法達到無效狀態嗎？怎麼樣？

Answer 1

這裏是如何將stm從here轉換爲coq。

Require Import Coq.Lists.List.                                         

Inductive alpha : Set := A | B | C | D. 

Fixpoint s1 (xs : list alpha) : bool := 
    match xs with 
    | C :: rest => s2 rest 
    | _ => false 
    end 

with s2 (xs : list alpha) : bool := 
    match xs with 
    | nil => true 
    | A :: rest => s2 rest 
    | B :: rest => s2 rest 
    | C :: rest => s3 rest 
    | _ => false 
    end 

with s3 (xs : list alpha) : bool := 
    match xs with 
    | D :: rest => s2 rest 
    | _ => false 
    end. 

這裏是定理指出STM不能達到無效狀態：

Theorem t : forall xs, s1 xs = false. 

但顯然它不是這個STM如此。在一般情況下，它可以通過歸納來證明。

如果您提供關於什麼是您的實際狀態機的更多信息，將會更容易爲您提供幫助。

Answer 2

對於模型檢查器來說，這似乎更像是一個問題，而不是定理證明者。

關於此問題一直存在Can Coq be used (easily) as a model checker?的問題，並且確實有一些關於使用Coq作爲模型檢查器的工作，例如參見https://github.com/coq-contribs/smc，但可能不容易將其用於您想要執行的操作。