Alguns artigos de projetos desenvolvidos com Z/Eves estao disponiveis em:ftp://ftp.cs.york.ac.uk/pub/leo/papers/Procurando no google da pra encontrar as dissertacoes de mestrado citadas nos artigos.Nota:Estes artigos nao sao um bom ponto de partida para entender Z nem Z/Eves, mas sao uteis em descrever como superar problemas com provas em Z/Eves e como medir o esforco empregado na mecanizacao de especificacoes. Como ponto de partida para mexer com Z/Eves, o Z/Eves User's Guide e essencial. Conjectura experimental:Dada uma operacao OP sobre o estado STATE, que e formada pela disjuncao das operacoes OP1, OP2, ..., OPn, cujas precodicoes OP1Sig, OP2Sig, ..., OPnSig sao calculadas atraves dos teoremas tOP1, tOP2, ..., tOPn, e possivel calcular a precondicao da operacao OP utilizando o algoritmo:ENTRADA DO ALGORITMO:1. Schemas que encapsulam precondicoes: OP1Sig, ..., OPnSig.2. Schema que encapsula precondicao da operacao OP, isto e:OPSig \defs OP1Sig \lor OP2Sig \lor ... OPnSig3. Teoremas de precondicoes tOP1, tOP2, .., tOPnALGORITMO:Build-Z/Eves-Proof-Script {let i = 1while (i<=n) { split OPiSiginvoke OPiSigcasesuse tOPi with disabled (OP1, OP2, ..., OPn, STATE) prove by reducefor EACH-COMPONENT existentially quantified in current goal do: instantiate (COMPONENT1__0'==COMPONENT1',COMPONENT2__0'==COMPONENT2', ...,COMPONENTn__0'==COMPONENTn') rewrite nextlet i = i+1} invoke rewrite next}Prova de conceito: ToyGenericProofDesing.zipEste topico esta aberto a discussoes, dado que e um resultado experimental e sem prova. Este reasoning sobre provas foi extraido do arquivo de prova da verificacao do Simple Kernel. Para estudantes do MEFES que tenham acesso aos arquivos de prova do simple kernel, podem verificar a aplicacao deste reasoning na prova da precondicao da operacao EnqueuePRIOQ.Nota: o formato usado para calcular a precondicao das operacoes OP1, ..., OPn utilizado neste algoritmo, baseia-se em escrever a assinatura do teorema de precondicao utilizando Schemas. Este raciocinio e explicado no artigo "Mecanizando o componente de navegacao do IBM CICS: um experimento do Grande Desafio". Behavioural Preservation in Fault Tolerant Patterns AbstractIn the development of critical systems it is common practise to make use of redundancy in order to achieve higher levels of reliability. There are well established design patterns that introduce redundancy and that are widely documented in the literature and adopted by the industry. However there have been few attempts to formally verify them with respect to behavioural preservation.In this work, we purpose an approach to specify such design patterns, called here fault tolerant patterns, using HOL. We use the theorem prover HOL4 to prove the compositionality and correctness of the fault tolerant patterns. We illustrate our approach by modelling three classical fault tolerant patterns: homogeneous redundancy, heterogeneous redundancy and triple modular redundancy. Our model takes into account that the original system (without redundancy) computes a certain function with some delay and is amenable to random failures.In order to prove that a fault tolerant pattern preserves the behaviour of its subsystems, we defined new notions of refinement. Systems engineers commonly accept the fact that fault tolerant patterns do not change the functionality of a system. However, this practise is not compatible with the classical refinement notions. Thus we defined axiomatic notions of refinement to prove that the formalised fault tolerant patterns preserve the behaviour of its subsystems.We also proved that our fault tolerant patterns