Hi, We implemented a tool to allow design-by-contract in Go by automatically generating pre and postcondition checks in code: https://github.com/Parquery/gocontracts.
However, the most interesting part of the design-by-contract, namely invariants, is still missing and I'd like to hear your feedback on how to implement it. In an OO language, invariants should hold after the constructor and after invocation of each public method. They are particularly interesting way to formalize the properties on your more complex contained data structures. For example, if you internally use a sorted slice to perform binary search on it for interval queries, an invariant would be that the slice is always sorted. Another example is a directed acyclic graph with an invariant that there should be no cycles. For a more detailed (and better) article on advantages of design-by-contract in general and invariants in particular, please see: https://cacm.acm.org/blogs/blog-cacm/227928-why-not-program-right/fulltext Right now, gocontracts operates on individual files. To add the invariants to a type, I thought about passing the package folder (instead of individual files) to gocontracts, inspecting the type comments and iterating through all the public methods associated with the type. Since there are no constructors in Go, I'd establish the invariants in all the public methods as additional pre and postconditions. I though that a documentation defining the invariants could look like this: // SomeType represents something. // // SomeType establishes: // * x >= 0 // * x < Width // * x < somePrivateProperty type SomeType struct { // ... } For some method: // SomeFunc does something. // // SomeFunc requires: // * x % 3 == 0 func (s *SomeType) SomeFunc(x int) { // ... } gocontracts would append the invariants of the type to the pre and postconditions and generate the checks as: // SomeFunc does something. // // SomeFunc requires: // * x % 3 == 0 func (s *SomeType) SomeFunc(x int) { // Pre-conditions switch { case !(s.x >= 0): // panic ... case !(x % 3 == 0): // panic ... // ... } // Post-conditions defer func() { switch { case !(s.x >= 0): // panic ... // ... } }() // ... } How do you like the idea? Is the syntax appealing? Would you mind if you could only disable/enable checks on per-package basis? In case gocontracts would still keep on operating on individual files, would it be confusing if it parsed all the other go files in the file's directory to read the invariants and then apply it to only the given file (and not establishing invariants on the functions defined in other files)? Thanks a lot for your feedback! Marko -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
