How can I find out if a specification is precise enough?

Using Coq
1

I am reading Software Foundations, chapter Logic. See here. There is an informal exercise that asks:

Are there any important properties of the function forallb which are not captured by this specification?

Here are the relevant types:

forallb: (?X -> bool) -> list ?X -> bool

All:     (?T -> Prop) -> list ?T -> Prop

forallb_true_iff: forall (X : Type) (test : X -> bool) (l : list X),
       forallb' test l = true <-> All (fun x : X => test x = true) l

I have proven this theorem with two variants of forallb that process the list in either usual or reverse order. So, the order of evaluation is not captured.

  • Is this the «important property» the book hints at?
  • How hard would it be to formally prove that forallb_true_iff nails forallb exactly up to the order of evaluation?
2

You can prove that any two functions satisfying that specification always produce the same result, so the only remaining differences would only concern implementation details, such as evaluation order or running time. It would be an exercise well adapted to the level of Software Foundations.