[ProofPower] HELP TO AN INCONSISTENCY PROOF!!

[Rob Arthan]

Thiago,

On Friday 21 May 2004 2:34 pm, Thiago Carvalho de Sousa wrote:
> ... My research is
> how to apply belief revision theory (an AI field) in
> software engineering specifications. This theory
> provides a way to keep consistency. More specifically,
> I'll try to solve modelling inconsistencies, which
> there are no inputs for which the operation is valid.
> And we can show this operation is `inconsistent' by
> demonstrating that its precondition is false. By the
> way,I'm going to ask you some others questions:
>
> 1) Suppose I have a very large Z specification with
> several 'inconsistent' operations. Do I have to check
> the pre-condition of each operation? Is not there a
> way to check the pre-conditions of the whole system?

You have to bear in mind that if you just give a set of of schemas comprising 
the operations of a system, then you're relying on informal conventions for 
the actual construction of the system as a whole. If you're going to do 
formal proofs, then you need to specify formally how the operations are 
combined in the possible executions of the system. There is a long tradition 
of not bothering to do this, but you're going to have to if you want to 
reason about the system as a whole. Then you'll have a single schema 
combining the individual operation schemas in some way and its precondition 
is what you'll need to calculate.

I think uou also need to bear in mind that once you start composing 
operations, it is not sufficient to prove that the pre-conditions of the 
individual operations are satisfiable (i.e., not false). For example if you 
have

STATE = [counter : {0, 1}]

DEC = [Delta STATE | counter > 0 /\ counter' = counter - 1]

then

pre DEC = counter = 1

but

pre (DEC; DEC) = false

I've attached Phil's corrected version of your specs and proofs with this 
example added.

>
> 2) For statistical history, some idea about how many
> people use Proofpower in the world for software
> development?

As it's available for free public download, I don't really know. For what it's 
worth, the tarball for version 2.7.3 has been downloaded about 70 times 
(ignoring me testing it) since I uploaded it on March 22nd.

In the early days (mid-90s) before ProofPower was open source, it was used by 
its then owner, ICL, and sold under licence to a small number of 
organisations whose main interest were in security proofs for applications 
they were not allowed to tell the world about.

These days the emphasis is more on safety-critical applications rather than 
security, although it is being used by one US user for security work. The 
main user group I know of is at QinetiQ, Malvern, where the group that Phil 
belongs to use it as part of a process for verifying avionics control 
systems. There are also users whose work I know of in several UK universities 
(most notably Kent and York). But that's just people whose work I know about.

Regards,

Rob.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rda-test-reply.doc.gz
Type: application/x-gzip
Size: 823 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040522/fd0050fd/attachment.bin>