CODEWITHSUNDEEP
logiccoqisabelleformal-verification
Huan Sun
Huan Sun

Reputation: 167

How to prove sequential commands C1; C2 can always execute to C2 if we know C1 always terminates?

I am using a theorem prover to demonstrate the progress of programs.

The semantics of a program are defined using a small-step relation, denoted as ctran, between program configurations. A program configuration is defined as (C,s) where C is a command and is a state. a valid execution is thus defined as (C1,s), (C1', s') \in ctran. we use ctran* to denote the transitive reflexive closure of ctran. The termination of a program is then defined as exists t, such that (C1, s), (term, t) \in ctran*. Now I already have (C1, s), (term, t) \in ctran*, How can I prove (C1; C2, s), (C2, t) \in ctran*

Upvotes: 0

Views: 43

Answers (1)

Yves
Yves

Reputation: 4236

In course material for semantics of programming languages the definition of sos_step expresses that skip (which is the equivalent of your term) is ignored when executed at the first step of a sequence. Then, the statement you wish to obtain is a consequence of associativity of sequence with respect to executions as expressed by theorem sos_sequence_aux.

Upvotes: 0

Related Questions