Personnes présentes
- Frédéric Boulanger
- Hai Nguyen Van
- Safouan Taha
- Frédéric Tuong
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
A state machine free model of Lustre
Burkhart presents a model of the synchronous programming language Lustre. It is based on a shallow embedding, representing "blocks" with potential feed-backs as stream-processing functions (assuming that streams are typed).
The shallow embedding provides basic operations for arithmetic and logic which
assume a null-element for non-existing values; with one exception (the test isNull)
all operations of the Lustre language are assumed to be strict extensions.
The resulting shallow-embedding called HOL/Lustre allows finally to write typical examples:
fun COUNTER⇩b⇩o⇩d⇩y::"(COUNTER⇩i⇩n stream × COUNTER⇩o⇩u⇩t stream) ⇒ COUNTER⇩o⇩u⇩t stream"
where "COUNTER⇩b⇩o⇩d⇩y (inp, out) =
(let ⟦init, incr, X, reset⟧ = inp;
⟦PC, C⟧ = out;
PC' = init -> pre (C); (* construction of state variables *)
C' = if reset then init (* construction of output variables *)
else if X then PC' + incr
else PC'
endif
endif
in ⟦PC',C'⟧)"
definition COUNTER :: "COUNTER⇩i⇩n stream ⇒ COUNTER⇩o⇩u⇩t stream"
where "COUNTER ≡ (loop COUNTER⇩b⇩o⇩d⇩y)" (* block with feedback *)
as well as
fun SPEED⇩b⇩o⇩d⇩y::"(SPEED⇩i⇩n stream × SPEED⇩o⇩u⇩t stream) ⇒ SPEED⇩o⇩u⇩t stream"
where "SPEED⇩b⇩o⇩d⇩y (inp,out) =
(let ⟦beacon, second⟧ = inp;
⟦diff, incr, late, early⟧ = out;
incr' = if beacon and (not second)
then 1
else if second and (not beacon)
then -1
else 0
endif
endif;
⟦diff',_⟧ = COUNTER ⟦0, incr', beacon or second, false⟧;
early' = false -> (if pre early then diff' >s 0 else diff' >=s M endif);
late' = false -> (if pre late then diff' <s 0 else diff' <=s -M endif)
in ⟦diff', incr', late', early'⟧)"
definition SPEED :: "SPEED⇩i⇩n stream ⇒ SPEED⇩o⇩u⇩t stream" where "SPEED ≡ (loop SPEED⇩b⇩o⇩d⇩y)"
which gives a classical example of a speed-controller with latency. Our encoding would be able to cope with float-variables.
Wrt. to the semantic construction of the operators of HOL/Lustre, the proceeding is as follows:
First, a null class is defined to represent datatypes with a null value, and 'a option is shown to instantiate this class. Then pairing via cartesian products as well as streams itself are proven to
live inside this class.
The streams in Lustre are modeled as streams (nat => 'a) of with 'ainstances of the null class. The null value represents a hole in a stream. Thus, Lustre can be seen as a language to define behaviors by composing operators on infinite streams of values. These streams may have holes in them, i.e. samples with no defined value.
In order to achieve compositionality of streams, the projection and weaving of streams are defined so that a pair ('a stream, 'b stream) is isomorphic to a stream of pairs ('a×'b) stream.
A key concept for proving properties with feedback ("recursive blocks") is Computational Consistency; it Computational consistency of a process P is defined as : if for all n, two streams a and b are identical up to the nth sample, then P(a) = P(b) at n. This means that P depends only on the past of the stream. This is the major weapon to prove via a kind of specialised induction properties on blocks with feedback, as long as they only consider the past in their input and feedback streams.
Strict computational consistency of a process P is defined as : for all n, if the nth sample of a is identical to the nth sample of b, then P(a) = P(b) at n. This means that P depends only on the current sample of the stream (it has no memory).
Compositionality of streams and computational consistency allow the definition of the semantics of networks of operators with feedback (an output stream is fed back to the input of an operator).
Then a Hoare-style semantics is defined, and a proof is made on a simple example of a counter, which is an adder fed back with its own output. For example:
theorem MySecondThm:
"COUNTER ⇘{⟦0, 1+1, true, true -> false⟧}⇙⊩ ( (λ ⟦_,C⟧. (C mod (1+1) =s 0)))"
unfolding assert''_def COUNTER_def
proof(auto simp: Lustre_basics.is_def_stream )
text{* The proof comes in two major stages: first, we have to establish
that the program observables are pointwise defined. We proceed by: *}
fix input n
show "is_def (loop COUNTER⇩b⇩o⇩d⇩y ⟦0, 1 + 1, true, true -> false⟧⟦n⟧)"
apply(rule COUNTER_def_preserve_pointwise[simplified COUNTER_def])
by(simp add: Lustre_types.is_def_pair plus_option_def)
next
show "snd⇩s⇩t⇩r⇩e⇩a⇩m (loop COUNTER⇩b⇩o⇩d⇩y ⟦0, 1 + 1, true, true -> false⟧) mod (1 + 1) ≐ 0 = true"
(is "snd⇩s⇩t⇩r⇩e⇩a⇩m (?H) mod (1 + 1) ≐ 0 = true")
proof(rule observer_induct)
text{* This induction in itself boils down to three parts. *}
text{* First, our invariant must be strongly computationally consistent. *}
show "!⟨λa. ((snd⇩s⇩t⇩r⇩e⇩a⇩m a) mod (1 + 1)) ≐ (0::Integer stream)⟩" by(simp)
next
text{* Second, our invariant must be true at the initial state. *}
show "snd⇩s⇩t⇩r⇩e⇩a⇩m (COUNTER⇩b⇩o⇩d⇩y (⟦0, 1 + 1, true, true -> false⟧, nil)) mod (1 + 1) ≐ 0⟦0⟧ = true⟦0⟧"
by(auto simp: sel_simps true_simp Let_def plus_option_def split: if_splits)
next
text{* Third, our invariant must be preserved. *}
fix n fix σ::"(Integer × Integer) stream"
assume "((snd⇩s⇩t⇩r⇩e⇩a⇩m σ) mod (1+1) ≐ 0)⟦n⟧ = (true⟦n⟧)"
then show "(snd⇩s⇩t⇩r⇩e⇩a⇩m (COUNTER⇩b⇩o⇩d⇩y(⟦0, 1+1, true, true->false⟧,σ)) mod (1+1) ≐ 0)⟦Suc n⟧ =
(true⟦Suc n⟧)"
(* und schlachtefatz *)
by(auto simp: sel_simps true_simp Let_def false_simp plus_profile.nonstrict_compute
split:option.split_asm split_if_asm)
qed
qed
Note: No state machine was harmed during this meeting.