Cálculo de precondição de operações compostas

Conjectura experimental:

Dada uma operação OP sobre o estado STATE, que é formada pela disjunção das operações OP1, OP2, ..., OPn, cujas precodições OP1Sig, OP2Sig, ..., OPnSig são calculadas através dos teoremas tOP1, tOP2, ..., tOPn, é possível calcular a precondição da operação OP utilizando o algoritmo:

ENTRADA DO ALGORITMO:

1. Schemas que encapsulam precondições: OP1Sig, ..., OPnSig.
2. Schema que encapsula precondição da operação OP, isto é:
OPSig \defs OP1Sig \lor OP2Sig \lor ... OPnSig
3. Teoremas de precondições tOP1, tOP2, .., tOPn


ALGORITMO:

Build-Z/Eves-Proof-Script {
let i = 1
while (i<=n) {
split OPiSig
invoke OPiSig
cases
use tOPi with disabled (OP1, OP2, ..., OPn, STATE) prove by reduce
for EACH-COMPONENT existentially quantified in current goal do:
instantiate (COMPONENT1__0'==COMPONENT1',
COMPONENT2__0'==COMPONENT2', ...,
COMPONENTn__0'==COMPONENTn')
rewrite
next
let i = i+1
}
invoke rewrite
next
}


Prova de conceito: ToyGenericProofDesing.zip



Este tópico está aberto a discussões, dado que é um resultado experimental e sem prova. Este reasoning sobre provas foi extraído do arquivo de prova da verificação do Simple Kernel. Para estudantes do MEFES que tenham acesso aos arquivos de prova do simple kernel, podem verificar a aplicação deste reasoning na prova da precondição da operação EnqueuePRIOQ.


Nota: o formato usado para calcular a precondição das operações OP1, ..., OPn utilizado neste algoritmo, baseia-se em escrever a assinatura do teorema de precondição utilizando Schemas. Este raciocínio é explicado no artigo "Mecanizando o componente de navegação do IBM CICS: um experimento do Grande Desafio".