1. 33

@nickpsecurity and @rwhaling both helped with this one.

  1.  

  2. 9

    Another implementation of contracts for Python, should you be interested: https://github.com/deadpixi/contracts

    1. 5

      I like that page for examples that illustrate clean contracts, an English description of each, and short code for each. That’s nicely done. The commanding words, requires and ensures, are themselves worth thinking about using for future languages. It conveys a dependency or situation a person new to this should pay close attention to. “Preconditions” sounds a bit weaker in comparison with “invariants” requiring a definition. What do you think about the wording angle?

      1. 2

        Oh wow this is so much better. Thanks for the find!

      2. 7

        Great post (aside from the crack at Racket, which is by far the best language in the Universe)! I would like to see a follow up that discusses the common complaints about contracts when mentioned to people:

        1. They have overhead at runtime! Of course, Eiffel supports turning off the checks in production—what does that mean in other languages?
        2. They clutter my code, and I still have to write validators to make things robust. You can’t crash a web handler because someone provided crappy input, so how do contracts help here?

        Those are the things I hear when I bring up DbC, most commonly.

        1. 5

          Great post (aside from the crack at Racket, which is by far the best language in the Universe)! I would like to see a follow up that discusses the common complaints about contracts when mentioned to people:

          Honest question, did it come across as a crack? I thought saying “Racket is not popular” would be a fairly neutral claim.

          They have overhead at runtime! Of course, Eiffel supports turning off the checks in production—what does that mean in other languages?

          Eiffel has pretty intricate runtime controls. Not only can you turn off the checks, but you can turn off specific kinds of checks (like “don’t check postconditions”) and turn off checks for specific classes. Other languages, at the very least, let you turn off checks in production.

          Ultimately, though, this line has the same issue as any other performance argument: are you sure the contracts are the overhead you should be worried about? If you’re worried about performance, run a profiler.

          They clutter my code, and I still have to write validators to make things robust.

          This is one of the (many) reasons why language-level support for contracts is handy. It’s easy for an IDE to hide contracts or hide everything but contracts. It also means the contracts can “look” elegant. I personally think Eiffel’s contract syntax is beautiful.

          Other than that, it’s admittedly a problem. And it may very well be that for some programs, the mental overhead of adding more LoC cancels out the safety benefit of adding contracts. But again, I think that’s something you should measure and not just use abstract reasoning.

          You can’t crash a web handler because someone provided crappy input, so how do contracts help here?

          I think client/server is one of those cases where contracts aren’t that useful. IMO DbC works best where you have complete control over the client code. That means its great for things like monoliths, internal components, and libraries (where “you” is “the user of the library”), less so for APIs or services.

          1. 2

            Honest question, did it come across as a crack? I thought saying “Racket is not popular” would be a fairly neutral claim.

            Not really! I wasn’t being super serious here… Racket does have a pretty great, and very flexible contract system, but yeah, not enough people use Racket. :)

            are you sure the contracts are the overhead you should be worried about? If you’re worried about performance, run a profiler.

            That’s always the best answer. The typical treatment of contracts, though, talks about that right up front. “Hey, look! You can have these turned on only in development and testing, and then when you go to production everything is great!” Of course, realistically, you didn’t catch all the bugs in testing and staging, so you’re hosed in production, too, but if you’ve turned off contracts, well, you have no idea why. But, you didn’t crash, and deny service to others, at the same time… Interesting problem.

            And it may very well be that for some programs, the mental overhead of adding more LoC cancels out the safety benefit of adding contracts.

            It’s not clear to me that this is a LoC problem so much as a DRY problem (Yes, I think those are separate). Contracts often overlap with validation code, in more than just a type checking way.

            I think client/server is one of those cases where contracts aren’t that useful.

            Right! But, in the new age of computing, I call out to a service for what might have traditionally been an “internal component.” So, either contracts will become broadly inapplicable in the world, or we figure out a way to adapt them to distributed use cases. Being able to customize how an assertion fails might be the simplest approach. In tests, it’s a full stop. In production, the contract drops the connection after first returning an appropriate error message, or whatever.

            I guess, in some ways, I wonder: can we pivot contracts into the formal way in which we do defensive programming?

          2. 1

            other aspect to 1: diagnosing failed expectations has a significant post-deployment cost too.

            1. 4

              One of best resources on that is “Release It!: Design and Deploy Production Ready Software…” by Nygard. He talks about a lot of ways to limit damage when problems hit post-deployment. One take-away I had, esp in example where whole airline went down due to interface error, was how much financial damage might be avoided for in return for a small price in developing contracts or leaving the checks in at least on boundaries outside team’s control. Big failures might have been avoided when a contract failure that got logged or brought to operators’ attention in real-time. Then, the other benefit of contracts kick in where they make the fix itself less likely to break things.

              1. 2

                Hmm, do you mean “fixing bugs”? Violations of contracts are essentially “bugs.”

                1. 2

                  Exactly. Violations of tacit, undocumented and unconsidered contracts are harder to fix than violations of contracts that were found when you satisfied the contract.

            2. 4

              Really enjoyed this, it helped me form more of an opinion about Clojure spec. I also enjoyed the references to assertions & other languages which focus on this. As I am a full-time Clojure developer, I thought I’d weight in with the little I know about Spec.

              I’m familiar with Clojure so I don’t want to make too many comments,

              From the context, I suspect this is supposed to be “I’m not familiar”

              It seems that Spec is more intended to help with runtime type checking,

              Kinda. You’re definitely supposed to have it off in production. It’s off by default. I’d like to see a change which allowed it to be turned on for dev, but I digress.

              The current API as I understand it is largely about having it on when running tests, and using the specs to do generative testing. You start from a “type” inferred by predicate (e.g. string?) and then run it against the other predicates, and do that until you get a valid match. Then you run that against the function and ensure the “out” contract is matched for all inputs.

              I think Spec has the major benefits you tout for contracts in your article. Clojure gets some of the contextual uses for free by handling “functions”, but does fall down on “loop variants” and “check contracts”.

              1. 4

                I really like that OP mentions the importance of contracts. An important use of contracts in programming is in concurrent programming. Sequential consistency and linearizability are often expressed in terms of “adhering to the contract of a (concurrent) object”. It seems very important to understand this notion of contracts before moving on to more advanced topics, e.g. to study the possible interleavings of multiple threads interacting with some shared object. That might be an interesting topic for a next post? And since contracts also intimately relate to model checking, viz. checking properties of semantical models, of programs, and I know OP is very interested in that topic, it might all come together as follows:

                1. Start with the notion of “objects” that encapsulate behaviour and data. Clearly, data is the “statica” and behaviour is the “dynamica” of some system. Each could be represented by the other.
                2. Introduce contracts as specifications, declaring intent or external expectations. They bridge the gap between the data and the behaviour: what expected performed behaviour can be proven by inspecting the data before/after some moment in time.
                3. Allow abstraction to specify classes of objects that share the same contract, arriving at Abstract Data Types.
                4. Introduce tools to verify that a given implementation adheres to its contract. Could be QuickCheck/fuzzing/random testing, or more formally by proving (inductively) in some logical system that contract clauses are never breached, or by model checking/finding that could produce a counter-example to disprove adherence to a contract.
                5. Explore alternative program semantics: what if exceptions could occur at random places (intentional failure), what if programs can crash at random places (extentional failure), what if programs are executed in parallel but isolated from eachother (intentional concurrency), what if programs could be executed in parallel and interfere (extentional concurrency)? How would that affect the correctness of an implementation with respect to its contract?

                One should also immediately be convinced that contracts are not more than a tool, e.g. an error or ommission in a contract could still cause errors or unexpected behaviour in programs. Important questions could be: when is a contract sufficiently detailed while leaving enough room for different implementations? What is refinement of contracts? What is composability of multiple contracts, e.g. could two contracts describe differently the same behaviour of some object or could we show that a contract holds given the assumption another contract holds? What is consistency of a contract? And, finally, is a contract even inhabitable? These questions could lead to a deeper understanding of programming, serve as a nice spring board to type theory, and I would therefore agree that contracts are an important notion for any learner of programming semantics.

                Thought provoking…

                1. 2

                  That ties to one of my pet peeves about the “modern correctness world”. People seem to think that each technique is at odds with every other technique, and you have to pick a side of “unit tests!” or “types!” or “contracts!” Where as you pointed out, they all synergize with each other. ADTs and contracts are related, PBT makes contracts more powerful, types reduce the load on unit tests, etc. Really “contracts can do things that tests can’t” isn’t an invitation to stop using test, it’s an invitation use both.

                  BTW, I loved your posts on bisimulation. Are you planning on doing any more?

                2. 3

                  For those that are interested, I wrote a small Design by Contract library for C++ that is part of Fire★ which you can see here. It prints nice messages with stack traces and either kills the program at that point.

                  Feel free to rip it out and use if it’s useful to you.

                  1. 2

                    Regarding footnote 2, in case anyone was curious, C# also has a way to mark methods and classes as obsolete which works in much the same way as Eiffel’s: https://msdn.microsoft.com/en-us/library/system.obsoleteattribute(v=vs.110).aspx

                    1. 1

                      Forgive me, but what do contract libraries offer that a normal if statement doesn’t? I guess for post conditions you don’t need to copy/paste. With go you can probably simulate that with defer statements.

                      1. 2

                        Contract libraries raise an exception if the condition fails. If statements move onto the second branch, which implies there’s an alternative behavior you want. Additionally, you’re not supposed to catch the contract failure. If the contract fails, the execution ends, full stop.

                        This makes them suitable for catching conditions that must be true. Something that you expect to never fail because you assume you wrote the program correctly. If it fails, there’s a bug in your program. In that case, you don’t switch to some conditional. You stop the program, find the bug, and fix it.

                        For the record, most people turn on contracts for development and testing and then turn them off for production.

                        1. 1

                          In terms of expressiveness, it depends on the formalism. They’re normally Hoare Logic or Boolean for SPARK. You can definitely emulate them in standard, programming constructs. A bigger benefit of dedicated statements for contracts is so both humans and tooling recognize them distinctly. The humans will use them to understand the interface requirements. The tooling can do a lot of things ranging from generating tests, proving things, or just selectively generating the conditionals for runtime program or not doing it. They might even be extracted for conversion into a totally, different tool.

                          You can implement your contracts with conditionals in beginning, end, and body of your code on top of the ones you use for implementation. It just gets messier without the tooling benefits. Well, there could be some for just if statements out there with enough money slushing around in CompSci for esp C# and Java. Let’s say not as easily get tooling benefits.

                          1. 2

                            static checking and tooling would be a great thing, but the article didn’t really mention it.

                            1. 1

                              Yeah, next version should probably highlight the tie-ins since just talking DbC in isolation might lead others to counter that same thing can be done with tests or something. Onto that. Eiffel, which popularized DbC, has a tool for generating tests from contracts:

                              https://www.eiffel.org/doc/eiffelstudio/Using%20generated%20tests

                              SPARK uses contracts in formally verifying code free of defects common in low-level languages such as C. Microsoft VCC uses separation logic for its contracts/assertions to… with much extra effort… prove heap safety for C code. They use it in Hyper-V. SIF at Cornell uses labels for information-flow security in web apps. Something similar was done with SPARK contracts later.

                              So, those are a few examples of ways tooling interacts with contracts in various projects.