0
$\begingroup$

Hoare Triple formalizes program correctness, which contains postcondition, program and precondition such as $\vdash P \{Q\} R$

Provided code snippet:

i := 0;
s := 0;
while i < N do
   s := s + max(arr[i]);
   i := i + 1;
od

The program's goal is to compute the sum of the maximum integers obtained from each element $arr[i]$, for $0 ≤ i < N$.

What is a proper Hoare Triple and loop invariant for this program? I’m stuck with prove of partial correctness because of loop invariant.

Improve this question
$\endgroup$
4
  • $\begingroup$ I cannot figure out the meaning of $\max(arr[i])$. Is $arr$ an array of arrays ? $\endgroup$
    – user16034
    Commented Feb 14, 2023 at 21:57
  • $\begingroup$ Hint: the invariant expresses that $s$ holds the partial sum of the terms from $0$ to $i$ excluded. $\endgroup$
    – user16034
    Commented Feb 14, 2023 at 21:59
  • $\begingroup$ What have you tried? Please check cs.stackexchange.com/help/how-to-ask $\endgroup$
    – Kai
    Commented Feb 14, 2023 at 22:03
  • $\begingroup$ @YvesDaoust yes, arr ist array of arrays of integers $\endgroup$
    – Bruce
    Commented Feb 14, 2023 at 23:07

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.