5 ms·

Forgetting about SPARK was a big whoops for me. (Lots of formal verification languages are based on contracts, like SPARK, Frama-C, and Dafny. I'm interested i

by hwayne 4y ago

Forgetting about SPARK was a big whoops for me. (Lots of formal verification languages are based on contracts, like SPARK, Frama-C, and Dafny. I'm interested in uses for contracts that aren't just formal verification, though!)

thesuperbigfrog 4y ago
>> I'm interested in uses for contracts that aren't just formal verification, though! Ada 2012 design-by-contract features aren't just for formal verification, they can be used in a general purpose way similar to Eiffel: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... Can you elaborate a bit more about the wanted features for a language with semantic relations?
- hwayne 4y ago
  An example off the top of my head would be writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. Another idea would be being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. I don't know how useful this would be in practice, but it seems interesting to me!
  - thesuperbigfrog 4y ago
    >> writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. That capability would be very useful. There are many cases where I have had to define serialization and deserialization functions for numerous objects and had to create so much "boilerplate" unit test code like you describe. It made me wish I was using a Lisp with built-in reader and printer functions. >> being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. This strikes me as very Haskell-ish, but could be quite useful to ensure certain properties or invariants.
    - nextstepguy 4y ago
      I use fuzzing for this. In fact that's the main case I use it for.

by hwayne 4y ago

thesuperbigfrog 4y ago

>> I'm interested in uses for contracts that aren't just formal verification, though! Ada 2012 design-by-contract features aren't just for formal verification, they can be used in a general purpose way similar to Eiffel: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... Can you elaborate a bit more about the wanted features for a language with semantic relations?

hwayne 4y ago
An example off the top of my head would be writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. Another idea would be being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. I don't know how useful this would be in practice, but it seems interesting to me!
- thesuperbigfrog 4y ago
  >> writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. That capability would be very useful. There are many cases where I have had to define serialization and deserialization functions for numerous objects and had to create so much "boilerplate" unit test code like you describe. It made me wish I was using a Lisp with built-in reader and printer functions. >> being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. This strikes me as very Haskell-ish, but could be quite useful to ensure certain properties or invariants.
  - nextstepguy 4y ago
    I use fuzzing for this. In fact that's the main case I use it for.