ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
128 stars 16 forks source link

Stdlib #423

Open mrjazzybread opened 1 week ago

mrjazzybread commented 1 week ago

Here is my pull request for the updated standard library. The goals of this update are to:

In order to achieve these two goals, we have removed or modified some of the definitions within this library. I will now go over them and justify them (note that some of these definitions are still in the standard library but only so that the tests still pass. In the future, these should be modified so as to not rely on these definitions):

Removed Definitions

References

Self explanatory: it does not make sense to talk about references within purely logical formulae.

Bitwise Operations

Although one could imagine a specification where one uses bitwise operations, these operations are out of place in a mathematical library. Additionally, these definitions are already present in the OCaml standard library and it does not make sense to duplicate them here. A better alternative would be to give those functions a gospel specification and allow users to use them if necessary in their specifications.

Operations on Pairs

Similar justification to bitwise operations.

Sequence Module

In the sequence module we remove the functions filter_map, fold_right, and renamed fold_left to fold In the case of filter_map and fold_right, these are just compositions of previously defined functions; in the case of the former filter and map, and in the case of the later fold and rev. The renaming of fold_left felt natural since there is only one fold function. I don't feel very strongly about these changes and if enough of a need arises, we could add them again.

List Module

The entire List module was removed from the standard library. The main reason is that the list type serves a similar purpose to sequence within specifications and it feels unnatural to have two very similar ways of reasoning over an ordered sequence of elements. Currently, to reason over lists in Gospel specifications, we just use a coercion that transforms them into sequences; in the future when we add some form of representation predicates to Gospel, we could have it so that the logical model of the type list is sequence.

Array Module

As i said with regards to references, it does not make sense to talk about arrays in a logical context

Bag Module

The occurrences function has been renamed to multiplicity. This also implied changing some of the tests.

The is_empty function has been removed since one could simple state b = empty as opposed to is_empty b.

The choose and choose_opt functions have also been removed. It is unclear why one would use these in a specification.

The map has also been removed. This is because it is very difficult to define it in the case that the parameterized function is not injective.

The fold function has also been removed. This is because it is impossible to define this function without also defining a canonical ordering of the elements within the bag.

The _exists and for_all predicates have also been removed as well as the partition function. To be honest, I do not remember the reasons why.

The conversion function to a sequence has also been removed since this would also imply a canonical ordering. The conversion from a sequence has also been removed, but I think that might have been a mistake.

Set Module

The compare function has been removed, no idea what kind of specification one could give it or why one would use it in a specification.

The remaining removed functions are similar to those from the Bag module and therefore I don't think there is a need to explain them again.

Order module

Since this module is about mathematical definitions it feels out of place to define a class of valid ordering functions for OCaml code. Although it makes sense to have this definition somewhere in Gospel, we should place it somewhere else.

System Variables and Exceptions

Similar Reasoning as to references.

Added Definitions

I don't think anything that we have added merits in depth explanation: mostly it was just defining all the functions we could and axiomatizing the rest. The majority of these definitions have been formalized and verified in Coq with a few exceptions these beings some axioms regarding cardinality and a few recently added axioms regarding subsequences.

Future Work

One glaring omission is the absence of axioms regarding arithmetic operations. These are absent since they are very cumbersome although fairly straight forward.

I would like have better notation for all of these Gospel data types: notably it would be pleasant to have pretty notation for the init and mem functions.

Naturally, if these changes are accepted, the tests should be changed so as to not rely on deprecated definitions. Personally, I think we should leave them as is and tackle them once we have ways of talking about ownership of OCaml values. This is because some of these conflicts, notably with references and arrays, are due to the fact that Gospel does not have a good way of talking about them in specifications. I believe that once we have added some form of representation predicates, that these tests can be rewritten quite naturally.

Finally, at some point we should separate these modules into distinct files. For now, since the standard library is still quite small, it is still manageable, however, as we add more things to it, it can very quickly become a big mess.