State-machines in Coq

Question

Can I use Coq to prove that a state machine cannot reach an invalid state? How?

@maxtaldykin Nothing so far, but lets say it's done with tail recursive functions like this: http://stackoverflow.com/a/9436688/2138090 — Olle Härstedt, Mar 01 '14 at 18:54
Just convert this OCaml code to Coq and prove theorem `forall x . s1 x == true` by induction. — max taldykin, Mar 01 '14 at 19:39
@maxtaldykin Thanks for checking :) , I'm still processing the information and how to apply it. I think I'll have to learn a little more Coq. This is my first question with my original use-case, if you're interested: http://stackoverflow.com/questions/22107667/proven-correct-receipt-module — Olle Härstedt, Mar 02 '14 at 21:49
I'll look at your other question but you need to show more commitment to solving your own problem. — max taldykin, Mar 03 '14 at 04:48
@maxtaldykin I know, I'm sorry! And grateful for your help. I'm still trying to conceptualize the problem in my head. — Olle Härstedt, Mar 07 '14 at 21:12

score 4 · Accepted Answer · edited May 23 '17 at 10:29

Here is how to translate stm from here to 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.

Here is the theorem stating that STM can't reach invalid state:

Theorem t : forall xs, s1 xs = false.

But obviously it is not true for this STM. In general case it could be proved by induction.

It will be easier to help you if you provide some more information on what is your actual state machine.

score -1 · Answer 2 · edited May 23 '17 at 11:55

-1

This seems more a question for a model checker than for a theorem prover.

There has been the question Can Coq be used (easily) as a model checker? about this, and there indeed is some work about using Coq as a model checker, see for example https://github.com/coq-contribs/smc, but it is probably not easy to use this for what you want to do.

edited May 23 '17 at 11:55

Community

1
1

answered Jan 20 '17 at 17:24

Freek Wiedijk

481
1
3
15

While this may theoretically answer the question, [it would be preferable](//meta.stackoverflow.com/q/8259) to include the essential parts of the answer here, and provide the link for reference. – Baum mit Augen Jan 20 '17 at 17:28
The answer essentially is: there is some work in this respect, but not really something that really is being applied. I'll edit my answer. – Freek Wiedijk Jan 20 '17 at 17:31
@baum-mit-augen Is my edited answer better? I hate it that I now have a -1 answer in my list, but do not know what to do about it. I would like to fix this! – Freek Wiedijk Jan 21 '17 at 08:15
Let me chime in -- I think you can make your answer into a great one by providing a (minimalistic) working example of how to use the library you gave the link to. – Anton Trunov Jan 21 '17 at 20:57

State-machines in Coq

2 Answers2