알고리즘의 정확성을 입증하십시오.

Question

누구든지이 질문에 답할 수 있는지 궁금합니다. 이전 시험지에서 나온 것으로 이번 해의 시험 준비를 알면됩니다.

이 질문은 너무 간단해서 완전히 잃어 버렸습니다. 정확히 무엇을 요구하고 있습니까? 최대 값을 찾으려면 다음 알고리즘을 사용하고 있습니까?

{P: x≥0 ∧ y≥0 ∧ z≥0 } 
if (x > y && x > z) 
max = x; 
else if (y > x && y > z) 
max = y; 
else 
max = z; 
{Q: max≥x ∧ max≥y ∧ max≥z ∧ (max=x ∨ max=y ∨ max=z)} 

대답은 알고리즘에 대한 가장 약한 전제 조건의 계산을 기반으로해야합니다.

어떻게 확인하나요? 그것은 단순 해 보인다.

감사합니다.

Answer 1

이 질문은 너무 간단해서 완전히 잃어 버렸습니다. 정확히 무엇을 요구하고 있습니까?

질문은 (프로그램을 읽고 분명히 작동한다고 말하는 것과는 달리) 미리 결정된 일련의 규칙을 엄격하게 적용하여 프로그램이 지정된대로 동작하는지 공식적으로 증명하도록 요청합니다.

어떻게 확인하나요? 다음과 같이

이 프로그램은 다음과 같습니다 if (y > x && y > z) max = y; else max = z;

에 대한

P1 속기와

if (x > y && x > z) 
max = x; 
else P1 

그래서 프로그램이 기본적으로 경우 - 당시 다른 사람이다. 호어의 논리는 경우 - 당시 다른 구조에 대한 규칙을 제공

{B ∧ P} S {Q} , {¬B ∧ P } T {Q} 
---------------------------------- 
    {P} if B then S else T {Q} 

손에서 프로그램에 대한 일반적인 경우 - 당시 다른 규칙을 Instanciating :

{???} max = x; {Q} , {???} P1 {Q} 
------------------------------------------------------------------------------------- 
{true} if (x > y && x > z) max = x; else P1 {Q: max≥x ∧ max≥y ∧ max≥z ∧ (max=x ∨ max=y ∨ max=z)} 

당신이 ??? 자리를 완료 할 수 있습니까?

Answer 2

@Pascal Cuoq - 두 번째 자리 표시 자에 ¬x> y & & x> z를 입력해야합니까? 그게 전부 증거 야? 아마 다른 뭔가가 필요 하겠지? 부적절한 답변을 정정 해 주실 수 있습니까?

P1 = if (y > x && y > z) max = y; else max = z; 
{B ∧ P} S {Q} , {¬B ∧ P } T {Q} 
---------------------------------- 
    {P} if B then S else T {Q} 

Instanciating the general if-then-else rule for the program at hand: 

{x > y && x > z} max = x; {Q} , {¬ (x > y && x > z)} P1 {Q} 
----------------- 
{true} if (x > y && x > z) max = x; else P1 {Q: max≥x ∧ max≥y ∧ max≥z ∧ (max=x ∨ max=y ∨ max=z)}