How to use correctly an universal quantifier

96 Views Asked by At

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] $$

  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?
  2. Did I use the allquantor correctly?

Thank you in advance for any advice. :)