0
다음 코드 단편에서 x는 숫자입니다.루프 불변성을 유도하는 방법은 무엇입니까?
{ y >= 0 }
z = 0
n = y
while (n > 0) begin
z = z + x
n = n – 1
end
무엇이 계산됩니까? 루프 불변성을 유도하는 방법을 보여주는 입증하십시오.
어떻게하면됩니까?
A
답변
0
주어진 X 및 Y에 대해 X * Y을 계산합니다.
처음에는 Z의 값이 0이고 N = Y (우리 루프에서 카운트 다운되는 루프의 변수)입니다.
루프는 Y 번 실행하고 실행될 때마다 X을 Z에 누적합니다.
마지막으로 N이 0에 도달하면 루프가 종료되고 Z의 값은 X * Y이되어야합니다.
+0
고마워하지만 루프 invariant 파생 시켜서 그것을 보여주는 방법을 알고 있습니까? – user2977595
2
이 예제는 모든 소프트웨어 검증 과정에서 입증 되었기 때문에 가장 정확한 프로그램으로 알려져 있습니다. 다음은 각 단계에 불변으로 프로그램의 목록입니다 :
{ y >= 0 } z = 0 // invariant: z = 0 n = y // invariant: n = y and z = 0 while (n > 0) begin // loop invariant: y * x - n * x = z z = z + x n = n – 1 end // Final invariant: n = 0 and y * x = z
이 예를 들어 모든 이론적 인 세부 사항은 my paper page 118로 제공됩니다.
나는 factoriel과 같은 숫자의 합계를 계산하지만 합계는 없다고 생각하십니까? 루프 invariant 부분에 대한 나는 아무 생각이 – user2977595