$\begingroup$
$\endgroup$
1
Precondition: true
int i = 0;
while (i < a.length && a[i] != x) {
i++;
}
Postcondition: (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ (i = a.length ∨ a[i] = x) }
As I read it, the program has no precondition to be established, thus the precondition is always true? Is it like an indicator: "This program has no precondition"?
-
2$\begingroup$ You have answered your question correctly. $\endgroup$喜欢算法和数学– 喜欢算法和数学2022年05月18日 22:47:59 +00:00Commented May 18, 2022 at 22:47
1 Answer 1
$\begingroup$
$\endgroup$
4
The program does have a precondition: true. Which means that it is fulfilled, regardless the state variables.
The annotation would still be correct with a stronger precondition, such as a.length > 0. truecannot be weakened, so it is the weakest precondition.
-
$\begingroup$ But true & a.length > 0 would only be true if a.length > 0. If a.length > 0 is the precondition it wouldn't make sense to use true as precondition too? $\endgroup$Rubus– Rubus2022年05月19日 12:41:52 +00:00Commented May 19, 2022 at 12:41
-
$\begingroup$ @Rubus: true is a valid precondition and so is a.length > 0. Besides this, I have no idea what you are trying to say. $\endgroup$user16034– user160342022年05月19日 13:32:08 +00:00Commented May 19, 2022 at 13:32
-
1$\begingroup$ I understand it now. I though you meant true AND a.length > 0 need to be true which would render true useless since the truth value of the statement would then only depend on a.length > 0. I'm sorry I find this topic confusing... $\endgroup$Rubus– Rubus2022年05月19日 13:32:24 +00:00Commented May 19, 2022 at 13:32
-
$\begingroup$ @Rubus: I never wrote true AND a.length > 0 (nor with && nor $\land$). $\endgroup$user16034– user160342022年05月19日 13:34:11 +00:00Commented May 19, 2022 at 13:34