Benedikt Becker 1bb0c818f5 Separate logical and program function Array.make ...

When defined as a `val function` the postcondition of the program function
`make` is just `result = make n v`, referring to the logical function `make`.
But the equality cannot be proven because array equality is not defined.

To facilitate proofs about results of the program functions `make`, this
commit separates the definitions of the logical function from the program
function `make`, so that the postconditions of the program function `make`
refer to the properties of the resulting arrey.

2021-01-15 12:39:37 +01:00

15 KiB

Raw Permalink Blame History

View Raw