Artur,
On Monday 09 February 2009 14:58:17 Artur Oliveira Gomes wrote:
> To represent that everything except "a" is unchanged in State, we use:
>
> %BV% %theta%(State \%down%s (a))' =
> %BV% %theta%(State \%down%s (a))
>
> But, using this,
>
> %SFT%Z
> %BV% NewState %def% [OldState : State]
Hi there,
I'm working on a specification and I'm a little bit confused.
Given a simple state,
%SZS% State %BH%%BH%%BH%%BH%
%BV% a: %bbR%
%BV% b: %bbB%
%EZ%%BH%%BH%%BH%%BH%%BH%
And one operation over that state,
%SZS% OpState %BH%%BH%%BH%%BH%
%BV% %Delta%State
%BT%%BH%%BH%%BH%%BH%
%BV% a = real
