I am using the Hoare-Logic to proof the correctness of an algorithm. One postcondition is, that all elements of a field $f$ are sorted in ascending order.
I am using the following statement to express this:
$$ s\geq 0 \wedge s\leq n-2 \Rightarrow f[s] \leq f[s+1]$$
with $n$ is the number of elements in $f$.
Now I am wondering if I should rather use an universal quantifier to express this. But then I am not sure how to use it correctly. I would do something like this:
$$ \forall s : s\geq 0 \wedge s\leq n-2 \Rightarrow f[s] \leq f[s+1] $$
- Do I have to use the universal quantifier to express that all elements in $f$ are sorted or can I use the first statement shwon above?
- Did I use the allquantor correctly?
Thank you in advance for any advice. :)