[Prev][Next][Index]

Consistency

REGARDING                Consistency
Dear Jim,

A few weeks ago I, asked you for a sample proof of the implication C
generated by empty, -| in the Deque trait (Larch book, p.172). I'd like to
thank you and your colleges very much for developing this interesting proof
for me !

I' m currently working on a specification of a simple door control system
(just for fun and to become more familiar with the Larch prover). While
doing that, some (at least for me) interesting problems arised.

The main trait consists of the following declarations and axioms:

DoorCtrlSystem(S): trait

includes Natural1, Door, Light, Timer, Button

introduces
	init: -> S
	[__, __, __, __]: D, L, T, B -> S
	
	timeImpulse: S -> S
	push: S -> S
	release: S -> S
	sensorOpen: S -> S
	sensorClose: S -> S
	
	door: S -> D
	light: S -> L
	timer: S -> T
	button: S -> B
	
	
asserts
	S generated by init, push, release, timeImpulse, sensorOpen, sensorClose
	S partitioned by door, timer, light, button
	
	\forall sys: S, d, d1: D, l, l1: L, t, t1: T, b, b1: B
	
	init == [closed, dark, setTime(0), up]; 
				
	push(sys) == [open(door(sys)), bright, timer(sys), down];
	
	release(sys) == 
		if not(door(sys) = closed) then
			if door(sys) = opened then [opened, medium, setTime(s(s(s(0)))), up]
			else [door(sys), medium, timer(sys), up]
		else sys;
	
	timeImpulse(sys) == 
		if (door(sys) = opened) /\ (button(sys) = up) /\ timeup(timer(sys)) then
			[closing, medium, timer(sys), button(sys)]
		else [door(sys), light(sys), tic(timer(sys)), button(sys)];
	
	sensorOpen(sys) == 
		if (door(sys) = opening) then 
			[opened, light(sys), setTime(s(s(s(0)))), button(sys)]
		else sys;

	sensorClose(sys) == 
		if (door(sys) = closing) then [closed, dark, timer(sys), button(sys)]
		else sys;
	
	door([d, l, t, b]) == d;
	light([d, l, t, b]) == l;
	timer([d, l, t, b]) == t;
	button([d, l, t, b]) == b;

Sort D is generated by closed, opening, opened, closing
Sort L is generated by dark, medium, bright
Sort T is generated by setTime: Nat -> T
Sort B is generated by up, down

In sorts D, L, T, B all generators are specified to be different from each
other
(e.g. up = down == false).

To keep the specification simple I used the following trick: I provided the
induction rule G1 "S generated by init, push, release, timeImpulse,
sensorOpen, sensorClose" instead of "S generated by [__, __, __, __]", which
would be the real truth. At the same time, I defined the observers on [__,
__, __, __]. This (possibly bad) trick allowed me to prove some useful
theorems about the system, that are valid on the state space restricted by
G1 (instead of the whole state space D x L x T x B, that makes no sense). 

The problem: 

After successfully proving the theorem

implies 
	\forall sys: S, d: D, l: L, t: T, b: B
	
	(button(sys) = down) => (light(sys) = bright); (T1)

and completing the theory, an inconsistency was detected:
button(sys) was reduced to b, light(sys) was reduced to l, thus
the theorem was reduced to (b = down) => (l = bright). By applying the axiom
bright = medium == false, you get b = down == false, which is inconsistent.

Completing the system of axioms without the above theorem will succeed and
not indicate any inconsistencies.

I believe that the reason for this behavior is my "trick".


The questions:

- Is my trick really bad ?
- Is it a good idea to "assemble" the specification of a system like my
little door control system using its components specifications (Button,
Door, etc.) ?
- If my trick is unsuitable, why did the succeeding completion of the theory
without theorem (T1) not indicate the inconsistency? (because it is not an
equational trait ?)
- Is there a way to detect the inconsistency more systematically (and not
only "accidentially" while proving a theorem). 

A more general question:

- Until now, I only worked with initial or final algebra semantics. Can I
specify monomorph abstract data types while using loose algebra semantics as
you do (any literature on this topic ?) ?

I hope this questions are not annoying you. Thank you very much.

Daniel