My Clojure is not good enough for me to come up with a short, efficient way to check "the resulting fields are never nil, unless they were already nil before" that would be appropriate for a postcondition.
Currently this postcondition is the only remaining bug in the update process that I know of. It fires because tools like the kio CLI tool patch application definitions by first fetching all current fields, making local modifications on these fields, and then pushing all of it to the server, which therefore receives a mixture of nil and non-nil fields. The postcondition asserts that there must be no nil fields at all in the result of created-or-updated-app, but this conflicts with sql/cmd-create-or-update-application! which expects all fields to be present.
My Clojure is not good enough for me to come up with a short, efficient way to check "the resulting fields are never nil, unless they were already nil before" that would be appropriate for a postcondition.
Currently this postcondition is the only remaining bug in the update process that I know of. It fires because tools like the
kio
CLI tool patch application definitions by first fetching all current fields, making local modifications on these fields, and then pushing all of it to the server, which therefore receives a mixture of nil and non-nil fields. The postcondition asserts that there must be no nil fields at all in the result ofcreated-or-updated-app
, but this conflicts withsql/cmd-create-or-update-application!
which expects all fields to be present.