ONE_PLACE_BUFFER =
 class 
   type Elem
   channel add, get : Elem
   value opb : Unit -> in add out get Unit
   axiom opb() is let v = add? in get!v end; opb()
 end

/* алгебраическая спецификация списка */
LIST_A =
 class
	type
	 List
	value
	 empty_a : List,
	 add_a : Int >< List -> List,
	 head_a : List -~-> Int,
	 tail_a : List -~-> List
	axiom all i : Int, l : List :-
	 [head_add]
		head_a(add_a(i,l)) = i,
	 [tail_add]
		tail_a(add_a(i,l)) = l
 end

/* Спецификация списка в виде процесса */
LIST = 
 extend LIST_A with
 class 
  channel
 	is_empty : Bool,
	add, head : Int,
	tail : Unit
  value 
	list : List -> in add, tail out is_empty, head Unit
  axiom all l : List :-
	list(l) is
		is_empty!(l = empty_a); list(l)
		|=|
		let i = add? in list(add_a(i,l)) end
		|=|
		if ~(l = empty_a) 
			then head!(head_a(l))); list(l)
			else stop
		end
		|=|
		if~(l = empty_a) 
			then tail?; list(tail_a(l)) 
			else stop
		end
 end

/* неправильная алгебраическая спецификация */
variable head_res : Int
axiom all i : Int, l : List :-
	[head_add]
	 list(l) || (add!i; head_res := head?) is
		list(l) || (add!i; head_res := i)

/* должна выполнятся аксиома */
all i,i1 : Int, l : List :-
	add!i1 || (list(l) || (add!i; head_res := head?)) is
		add!i1 || (list(l) || (add!i; head_res := i))

/* примеры применения комбинатора interlock (++) */
value e,e1,e2 : T
channel c,c1,c2 : T
variable x : T

x:=c? ++ c!e is x:=e
x:=c? || c!e is (x:=e) |^| ((x:= c?; c!e)|=|(c!e; x:=c?)|=|(x:=e))

(x:=c1? |=| c2!e2) ++ c1!e1 is x:=e1
(x:=c1? |^| c2!e2) ++ c1!e1 is x:=e1 |^| stop

x:=c1? ++ c2!e is stop
x:=c1? || c2!e is (x:=c1?; c2!e) |=| (c2!e; x:=c1?)

/* правильная аксиома head_add*/
axiom all i : Int, l : List :-
	[head_add]
	 (list(l)++add!i) ++ head_res := head? is
		(list(l)++add!i) ++ head_res := i