[ProofPower] HELP TO AN INCONSISTENCY PROOF!!

[Philip Clayton]

Thiago,

There were a few syntactic issues in your example:
- `;' needs to be used in schemas, rather than `,' to separate
- declarations in the signature part
- conjuncts in the predicate part
- a schema can't have free variables, e.g. set1' in STATE1

There were also a few typing problems which I took the liberty of 
tidying up!

Also, from a cosmetic point of view
- you don't need `;' to finish Z paragraphs (unlike ML 
declarations/expressions)
- you don't need an =SML before Z paragraphs, they go in =TEX sections

In example 1, OPERATION_ADD_SET1 doesn't necessarily make set1 greater 
than set2 --- it only does this if
- the input object? is not already in set1and
- set2 is unchanged, i.e. you must say set2' = set2
Given that extra condition we can show this operation is `inconsistent' 
by demonstrating that its precondition is false. Presumably that's what 
you meant by inconsistent: there are no inputs for which the operation 
is valid(?)

Similarly for example 2. I replaced the given set OBJ by the set BOOL as 
this is what they are.

Hope that helps
Phil.


Thiago Carvalho de Sousa wrote:

>Hi All,
>
>I´m newbie in Proofpower and I´d like to have some
>help to prove an Z specification inconsistency using
>ProofPower. It is a modelling inconsistency, where the
>description of an operation conflicts with a state
>invariant. More especifically, I´d like a script to
>detect this kind of inconsistency. I´m sending to you
>a .doc file with 2 examples about what I´m trying to
>do. Thanks in advance!
>
>Best regards,
>
>=====
>Thiago Carvalho de Sousa
>Msc Student 
>University of São Paulo
>
>
>	
>		
>__________________________________
>Do you Yahoo!?
>Yahoo! Domains – Claim yours for only $14.70/year
>http://smallbusiness.promotions.yahoo.com/offer 
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test-reply.doc.gz
Type: application/x-gzip
Size: 653 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040521/fdc424f8/attachment.bin>