Which programming language are you using? It looks to me like you need exhaustiveness checking for pattern matching. Languages like Scala, OCaml, Purescript or Haskell support this out of the box.
Am I overlooking something?
Am I overlooking something?
I as a developer can go through the cases and reason that those cases are actually exhaustive and move on. Problem is that this is time consuming and one would need to check everything every time the partitionings change (which happens).
Some Youtube videos: https://www.youtube.com/results?search_query=property+based+...
Article by author of Hypothesis, the property-based testing framework for Python: https://increment.com/testing/in-praise-of-property-based-te...
Pycon talk on how Contracts + PET gets you integration tests: https://www.hillelwayne.com/talks/beyond-unit-tests/
An article from the property-based testing series on the blog F# for Fun and Profit: https://fsharpforfunandprofit.com/posts/property-based-testi...
My suggestion:
Must you have partial functions? Maybe you can model your data more tightly? If your conditions are too complex, maybe you could decompose them?
A big reason I like ADTs with concise syntax is to model data with nearly¹ no room for invalid or useless data. Then all¹ functions are total and matches are checked for exhaustiveness. A nice matching syntax on top makes mistakes easy to spot.
Not sure how to help with formal verification or exhaustiveness on partial functions.
¹ I don't model everything absolutely precisely, but deviations are more of an exception rather than the rule. Then they can be made apparent and reasoned about.