# Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

```Artur,

On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote:```
```
>The problem is: only for those cases,
>what I choose as witness does not satisfy the predicate.

Well, any sequence of length 1 (or zero?) does for the
first case. Proof attached.

If you still can't crack the other two send me your
best attempt.

Roger

```
```(*01*)

=SML
open_theory "z_library";
delete_theory "temp";
new_theory "temp";
new_parent "z_reals";
=TEX

(*defs*)
�Z
� TYPES ::= AA | BB | CC
�

�ZAX
� TYPE :  � TYPES
�������
� TYPE = {AA, BB}
�

�Z
�EXAMPLE � {a:TYPE; b:� � (a,b)}
�

�ZAX
� Example :  EXAMPLE
�

�Z
�S_EXAMPLES � {s:seq EXAMPLE |
�       � i,j: dom s
�       | i � j � � m1,m2: ran s
�                       | m1 = s(i) � m2 = s(j)
�                               � m1.2 � m2.2}
�

�Z
� S_Example �  �Example�
�

�ZAX
� S_Example2 :  seq EXAMPLE
�������
� dom S_Example2 = {1}
�

(*State*)
� AState �����������
� a, b, c: S_EXAMPLES
���������������

(*init of State*)
� InitAState �����������
� AState'
���������������

�Z
� IA_State �  (a' � S_Example2, b' � S_Example2, c' � S_Example2)
�

(*02*)

� Sch �����������
� a:�;b,c:�
���������������

� Sch1 �����������
� Sch
�������
� a=true
���������������

� Sch2 �����������
� Sch
�������
� b=10
���������������

�Z
� NSch � Sch1 � Sch2
�

(*Schema*)
� BState �����������
� var: NSch
���������������

(*init of State*)
� InitBState �����������
� BState'
������
� var' � Sch2
���������������

� CState �����������
� counter: �
���������������

(*init of State*)
� InitCState �����������
� CState'
���������������

�Z
� State � AState � BState � CState
�

�Z
� St � [StComp : State]
�

(*03*)
� Op1 ������������������
� �St
�������
� � State; State' |
�       StComp = �State � StComp' = �State' �
� counter' = counter + 1 �
�       �(State \�s (counter))'
�               = �(State \�s (counter))
��������������������������������

(*Initialization Proofs

Is it this correct? If so, how can
its initialization be proved?*)

push_pc "z_library_ext";

(*01*)
set_goal ([], �� AState' � InitAState�);
a (z_�_tac �IA_State�);
a (rewrite_tac [z_get_spec �InitAState�, z_get_spec �AState�,
z_get_spec �S_EXAMPLES�, z_get_spec �IA_State�, z_get_spec
�S_Example2�,
z_get_spec �Example�]);
a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
THEN asm_rewrite_tac[]);

(...)

(*02*)  set_goal ([], �� BState' � InitBState�);
(...)

(*Precondition Proofs *)

(*03*)  set_goal ([], �� �St � pre Op1�);
(...)
```
```_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
```