State-machines in Coq

상태 시스템이 유효하지 않은 상태에 도달 할 수 없음을 증명하기 위해 Coq를 사용할 수 있습니까? 방법?State-machines in Coq

2014-03-01 Olle Härstedt

어떻게 상태 시스템이 나타 납니까? 너 뭐 해봤 니? –

@maxtaldykin 지금까지는 아무것도 아니지만 다음과 같은 꼬리 재귀 함수로 끝났다고 말할 수 있습니다 : http://stackoverflow.com/a/9436688/2138090 –

이 OCaml 코드를 Coq로 변환하고 정리 forallall forallall x를 증명하면됩니다. s1 x == 참 '유도에 의해. –

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에 대한 사실이 아니다. 일반적으로 그것은 유도에 의해 증명 될 수있다.

실제 상태 머신에 대한 정보를 더 제공하면 도움이 될 것입니다.

출처

2014-03-03 04:45:38

-1

이것은 정리 검사기보다 모델 검사기에 더 많은 질문입니다.

이 문제에 관해서는 Can Coq be used (easily) as a model checker?이라는 질문이 있습니다. 예를 들어 https://github.com/coq-contribs/smc과 같이 Coq를 사용하는 방법에 대한 작업이 있지만 실제로는 원하는대로 사용하지 않는 것이 좋습니다.

출처

2017-01-20 17:24:17

이것이 이론적으로 질문에 대답 할 수 있지만 여기에 대답의 핵심 부분을 포함하고 참조 용 링크를 제공하는 것이 바람직합니다 (// meta.stackoverflow.com/q/8259). –

답은 근본적으로 다음과 같습니다.이 점에서 약간의 연구가 있지만 실제 적용되는 것은 아닙니다. 내 대답을 편집 할게. –

@ baum-mit-augen 제 편집 된 답변이 더 좋습니까? 나는 그것이 내 목록에 -1 개의 답을 갖고 있지만 그것에 대해 무엇을해야할지 모른다는 것을 싫어한다. 이 문제를 해결하고 싶습니다! –

답변

관련 문제