Überprüfung: Kombinieren Korrektheit Aussagen

Question

Die Frage ist:

 P1 {C} Q1 
------------------------- 
    P1 && P2 {C} Q1||Q2 

Ist diese Regel gültig?

Wie würde ich so etwas angehen? Ich kann nur versuchen, ein Beispiel zu finden, wo es falsch wäre.

Ich habe versucht, damit zu kommen, so dass die Kombination von P1 & & P2 beide Q1 und Q2 falsch machen, aber ich denke an keine. Also im Sinne dieser Gültigkeit, aber ich weiß nicht, wo ich es beweisen soll ... Der Text für diese Klasse ist absoluter Unsinn und ich kann online keine Ressourcen für die Kombination von Korrektheitsaussagen finden ...

Answer 1

Ich nehme an, das sind Hoare Triples, normalerweise {P} C {Q}; Ich verwende auch Wikipedia als Referenz.

So die Regel:

 {P1} C {Q1} 
----------------------- 
{P1 && P2} C {Q1 || Q2} 

ist gültig!

Intuitiv ist es ganz klar, wenn Sie die Logik unterstehen:

• {P1} C {Q1} bedeutet: Jedes Mal, wenn P1 hält, wird Q1 hält nach C Befehl ausgeführt wird.
• Sie wissen, dass, wenn P1 && P2 gilt, P1 gilt.
• Sie wissen, dass, wenn Q1 gilt, Q1 || Q2 gilt.

Sie können diese Aussagen Stück zusammen, um zu sehen, warum die Regel gültig sein muss: P1 && P2P1 schon sagt, also, wenn Sie C ausführen, erhalten Sie durch Annahme Q1, die Q1 || Q2 impliziert.

Daher {P1 && P2} C {Q1 || Q2}, wann immer Sie annehmen, {P1} C {Q1}, die genau das ist, was Ihre Regel angibt.

Formal können Sie die folgende Regel (Auszug aus Wikipedia) verwenden:

Consequence Regel

P' -> P, {P} C {Q}, Q -> Q' 
--------------------------- 
     {P'} C {Q'} 

, wo man einfach P' als P1 && P2 gesetzt, P als P1, Q als Q1 und schließlich Q' als Q1 || Q2.