Review: How Programming Languages Will Co-evolve with Software Engineering

Until recently, programming languages have been developed with little consideration for programming environments and tools, with the notable exception of Smalltalk, which was co-developed with an elaborate environment from the start.  Murphy-Hill and Grossman note in their paper "How Programming Languages Will Co-evolve with Software Engineering: A Bright Decade Ahead" (Future of Software Engineering, 2014) that this situation is changing, and provide seven predictions on the convergence of programming languages and software engineering (or, more precisely, programming environments and tools) in the next decade.

They predict that future programming languages will be designed with integrated development environments (IDEs) and social networks in mind.  One example they give for the former is the addition of dot notation to F#, allowing a syntax such as x.Length in addition to the functional length(x).  (Note, though, that in F# these have different meanings.)  The authors claim that the primary benefit of this notation is the ability of the IDE to provide code-completion for method (or function) names when typing "x."; this facility doesn't (yet) exist for the functional notation.  I have my doubts about this being the major reason for the inclusion of members in F#, but it could certainly be a reason for introducing dot notation as syntactic sugar for function calls in new languages.

Another prediction is that source code will no longer be limited to a single sequence of characters, instead being replaced by multiple simultaneous views.  Multiple views are already available through the use of various tools; what I would call refactor-and-undo is probably the most widely used method, but there are various tools specifically targeted at showing multiple views of a program.  These multiple views can be stored together as the official representation of the program, instead of being generated from a single "ground truth" consisting of ASCII (or unicode) strings.

Murphy-Hill and Grossman expect that future language design will be influenced by controlled experiments on how programmers use language features and to what extent.  With the widespread availability of open-source projects, it is possible to study this rigorously, and select language features based on what really works "in the wild." This is already happening to some extent with existing languages, such as C#.  I would advocate some care when using this method, since we know that some programming features take a long time to achieve adoption; a case in point is functional-programming techniques (see the last prediction below).  We should be careful not to eliminate good ideas just because they don't receive a wide following in the short term.

Turning to other technologies, the next prediction is that formal verification will become a reality for developers, rather than being limited to a small group of highly experienced researchers.  This will require the development of proof assistants that are stronger and more usable than those available today.  Obviously, there is a lot of work to be done before the use of formal verification becomes widespread, but advances in this area provide some support for the authors' optimism.

Gradual typing is a technique that allows developers to write programs with little or no type information.  As the programs mature, types can be added in order to raise the level of confidence in the correctness of the program by making more properties statically checkable. Murphy-Hill and Grossman predict that gradual typing will become more widespread in new programming languages, and will expand to include properties that can be expressed as types but aren't available in popular contemporary languages.

Existing programming languages are being used in new domains, such as parallel and distributed programming and big data, even though these languages aren't particularly suited to these domains.  The success of Erlang is an example of how well a language built from the ground up to support distributed computation can do when applied appropriately. Murphy-Hill and Grossman predict that newer languages will focus more on new paradigms at the expense of traditional single-user (and often still single-threaded) applications.

This is related to the final prediction, which is that functional-progrmming concepts will become more widespread, and the distinction between functional and imperative (or object-oriented) programming will be more and more blurred.  This trend is already happening, with the introduction of function objects ("lambdas") into popular languages such as C++, Java, C#, and Ruby, and with mixed languages such as Scala.  First-class function objects are one primary feature of functional programming; the other is the use of immutable data, which is particularly important in distributed applications.

There is a recent (and not so recent) body of work that points in the direction of each of these predictions.  Unfortunately, there are many influences on the design of programming languages, and various features of currently-popular languages were not really designed but added without serious consideration.  I am therefore not quite as optimistic as the authors; however, the points they make are insightful and the paper is well-worth reading.  Be sure to put a link to the paper in your 2024 calendar, in order to see which of the predictions will be realized by then!

Xtend, the Gentle and Functional Java

I didn't want to learn yet another programming language.  But I had to.

I needed to create an Eclipse editor for a domain-specific language, and I needed to customize content-assist and completion.  A friend recommended Xtext as a quick way to get an Eclipse editor with all the goodies up and running.  And it was quite easy to start with; I had to translate my ANTLR grammar into Xtext, which wasn't too painful, and within a day or so I had a working editor for my DSL.

The next step was to add custom content-assist to the editor.  This turned out to be relatively easy as well, except that the file Xtext generated for me was in this new language, Xtend.  So I had to learn the language.  Unlike quite a few other people I know, I first read the manual.  I admit I did this reluctantly, but as I kept reading I got more and more excited.

I've been using Java for many years, both in teaching and in developing applications.  It is certainly nicer than C++, and the refactoring support in Eclipse is wonderful, but there were other languages I used in the past that I enjoyed much more than Java.  Common Lisp, especially on the Lisp Machine, was a great language with a great environment.  Scheme was a special pleasure, being a very compact yet extremely powerful language.  In contrast, Java is very limiting and extremely verbose!

First, the substance.  I am a great fan of functional programming; it is a limiting yet at the same time liberating paradigm.  You don't get to make any assignments or other state changes; in return, the computation model is very simple and similar to standard mathematics.  Functional languages enjoy referential transparency, which means that the same expression in the same environment will always yield the same value.  In contrast, when side effects are possible, it is possible to call the same function or method multiple times and get different results each time, since something in the environment may have changed.  While object-oriented programming seems to be all about changing state, it is still possible to use functional-programming techniques to minimize state changes to those places where they are really useful.  Item 15 of Joshua Bloch's excellent book Effective Java (2nd Edition) is "Minimize mutabililty."  And Bertand Meyer, designer of the Eiffel programming language, expounds in his classic text Object-Oriented Software Construction (2nd Edition) on his Command-Query Separation Principle.  This principle advocates minimizing state changes, and using functional programming techniques inside object-oriented programs as much as possible.  The Scala language is a more recent attempt to reconcile the functional and object-oriented programming styles.  Java allows a functional programming style, but makes it unnecessarily difficult.  (A ray of hope, though: Java 8 is going to have lambda notation!)

And then, there is the form.  Java is obnoxiously verbose, especially in its requirements for types everywhere.  I'm not necessarily objecting to strong typing here, but even with strong typing there are many type inferences that the compiler can make.  For example, the fact that I have to write something like this is infuriating:

HashMap<String, List<String, Integer>> map = new HashMap<String, List<String, Integer>>();

One way of thinking about Xtend is as a simpler syntax for Java.  The Xtend compiler does extensive type inference, and most type specifications are optional.  But Xtend is much more than that.  It provides many conveniences, and is particularly well-geared to the use of functional techniques.  Functions ("lambda expressions") are an essential part of the language, and are a pleasure to use and read.  They simplify a lot of the boilerplate code needed in Java for callbacks of various kinds.  In addition, Xtend libraries supply many utilities in the functional style, and these look like an integral part of the language due to Xtend's extension capabilities, which allow external libraries to add methods that can be called as though they existed in the original Java classes.  Another great convenience is a much enhanced switch statements, which, among other things, can switch on types without requiring type casts.

At the same time, Xtend compiles directly into (readable) Java, not even into bytecode.  So it is 100% compatible with Java, and can be used in any combination with Java classes.  For example, Xtend classes can inherit from Java classes as well as the other way round.  Xtend is well-integrated with Eclipse, and offers most of the conveniences of Java development, including debugging the Xtext sources.  The major lack is in refactoring, although Rename, for example, is available using the Alt-Shift-R shortcut.

If you are stuck with Java but want a nicer syntax, I recommend that you take a good long look at Xtend.  You can start with the 50-second video on the Xtend website, then read the manual; surprisingly, it is quite readable!

#Xtend #FunctionalProgramming #Java

Review: Mars Code

Despite a few spectacular failures (such as the Mars Climate Orbiter and Mars Polar Lander), NASA is one of the top organizations worldwide in Systems and Software Engineering.  The Mars rover Opportunity has recently celebrated ten years of operation on Mars, and the newer Curiosity has been operating since August 2012, after a landing maneuver of unprecedented complexity.  This is quite a feat, considering the fact that the nearest repair technician is over 30 million miles away, and communications delay is about 15 minutes on average.  How do they do it?

The paper Mars Code by Gerard J. Holzmann (Communications of the ACM,  Feb. 2014) gives a rare glimpse into the process used in programming the Mars rovers.  It focuses on three methods used to reduce the risk of failure.  An important feature of all three methods is the use of automation.  The first consists of a set of risk-related coding rules, based on actual risks observed in previous missions.  For example, one rule requires the code to pass compilation and static analyzer checks without any warnings.  Another requires the code to have a minimum assertion density of 2%.  The assertions are enabled not only for testing, but also during the mission, when violations place the rover into a safe mode, during which failures can be diagnosed and fixed.  All the rules are checked automatically when the code is compiled. 

The second method consists of tool-based code review.  Four different static-analysis tools are used, with an automated system to manage the interaction between developers and reviewers in response to tool warnings.  In over 80% of the cases, developers agreed with the warnings and fixed the code without reviewer intervention.  An interesting observation Holzmann makes is that there was surprisingly little overlap between the between the warnings issued by the four tools. Apparently, each tool has its own areas of strength, and they are different enough that it is useful to use them all.

The third and strongest method is the use of a model checking tool for race conditions, one of the most difficult types of bugs to discover.  This cannot be done for the whole code base, but was used extensively in the Curiosity mission to verify critical multithreaded algorithms.   In some cases, the tool works directly from the C source code.  For larger subsystems, input models had to be prepared manually in the language of the model checker; this can reduce the input size by over one order of magnitude.

The challenges faced by NASA are obviously unique, and are very different from those involved in cloud-based mobile applications, to take a popular example.  There are many papers and books describing methodologies for developing such systems.  However, developing safety-critical systems for cars and aircraft, medical devices, and power grids, or financial systems that must be resilient to faults and deliberate attacks, requires reliability levels similar to those of NASA.  For developers of such systems, papers such as Holzmann’s should be required reading.

A related article you may want to read is They Write the Right Stuff, by Charles Fishman.  This article, from 1996, describes the culture of the group that wrote the software for the space shuttle, and how their development process led to the very high quality of their product.  For example, whenever a mistake was found in the code, it was traced to the corresponding problem in the process that allowed the mistake to be written and pass reviews and testing.  Then, the team investigated what other bugs could have been caused by the same process failure.  In this way, a bug in the control of the shuttle's robotic manipulator arm was traced back to a certain type of problem.  When investigating other effects of the same problem, a much more serious bug was found in the control of the high-gain antenna.  The bug was fixed before it had a chance to manifest itself.

It takes a lot of discipline and investment to work this way, but the result is a much better, more reliable product.  Sometimes it isn't all that important; other times, it's the difference between life and death.

Design by Contract and Refactoring

I am a great believer both in refactoring and in design by contract.  How do these two work together?

First, contracts are a great help when refactoring.  The first thing you need to know when you refactor a piece of code is what it is supposed to do.  This tells you what you can and can't do with it, and, no less important, what would be useful to do with it.  If it's an arbitrary set of statements, say part of an existing method you are trying to extract into a new method, there's little to help beyond reading the code and trying to figure out what it does and how it fits with the rest of the code.  (Even then, there are tools that try to deduce a contract for an arbitrary piece of code; more on that in a later post).  But if it's a method, you should have more help.

If you have a good suite of unit tests, you can try to look at the tests of that method to figure out what it's supposed to do.  But it's much easier if you have a contract attached to the method; the contract should give you a lot of the information you need.  For example, suppose you want to move one or more methods and fields from one class to another (perhaps you are using Pull Up Method, Push Down Method, or just Move Method).  In that case, you should check the contracts of moved methods to see how they fit in their new class.  Are the invariants of the new class maintained by the moved methods?  Are the contracts of the methods still valid, taking inheritance into account?  Nasty bugs can result if the answers are negative.

On the other hand, refactoring may require corresponding changes in existing contracts, as well as the creation of brand-new contracts.  In other words, contracts need to be refactored together with the associated code.  This is an added burden, which may well be an obstacle to the use of the design-by-contract methodology; not only do I have to invest effort in creating the contracts in the first place, I also have to refactor them later.  Why should I bother?

There are several answers to this complaint.  First, consider the alternatives.  You may be flying blind, trusting only on your undocumented understanding of the code.  In that case, good luck to you; you'll need it.  If you follow an agile methodology, such as Extreme Programming, you should have an extensive suite of unit tests to help you refactor.  Unit tests are very vulnerable to change in the code, since they are attached to small units of code.  This means that any shift in responsibilities is likely to invalidate some tests, which will then have to be refactored or completely rewritten.  So there's always the need to refactor associated artifacts when you refactor the code.

Having contracts can significantly reduce the amount of detail in unit tests, and even the total number of unit tests.  This is due to the fact that a major part of the responsibility usually given to unit tests is now taken by the contract.  All that the tests need to do is exercise the system, but correctness checking (or a large part of it) is now done by checking the contracts.  So now you can have higher-level tests that exercise the system, instead of unit tests for each class and method.  For example, suppose you are implementing a cryptographic algorithm such as RSA.  A test that creates a random key, then encrypts a random data buffer, decrypts it, and checks that the result is the original data, is guaranteed to exercise almost all of your cryptographic code.  Moreover, this test can be used on many different implementations.  In contrast, the internals of the implementation can vary widely, since there are many ways to implement the large-number arithmetic operations required for RSA, and their efficiency will be different under different circumstances.  By having an application-level test augmented with contracts, the burden of refactoring tests is reduced to almost nil.

This still leaves the requirement of refactoring contracts, and the question of how much refactoring tools can help.  In order to understand that, it is necessary to examine the relationships between code refactorings and contracts.  On the simplest level, contracts are treated just like code. For example, when renaming a method, all references to it in the code must be appropriately modified; so must all references in assertions. Similarly, a method may be eliminated when it is not used anywhere, including in assertions.  Contract-aware tools should find these kinds of relationships easy to perform automatically.  Of the refactorings listed in Fowler's Refactoring book, 32% do not interact with contracts except possibly in this way.  These are mostly syntactic refactorings such as Remove Parameter or Rename Method, or those that eliminate classes or methods, such as Inline Class and Inline Method.

Some contracts affect the applicability of certain refactorings.  As mentioned above, a method should only be moved if it won't violate the invariant of its new class.  (Of course, it might be possible to modify that invariant to accomodate the moved method; this can be done in a separate step, before moving the method.)  13% of Fowler's refactorings have this nature.

Some refactorings require the creation of new or modified contracts.  The most extreme case is Extract Method, which creates a new method out of arbitrary code.  Discovering the contract for arbitrary code is impossible in general, although some tools can discover partial contracts.  Another example is Create Superclass, which can create contracts for new methods based on existing contracts in subclasses.  59% of Folwer's refactorings fall into this category (which includes 4% that are also included in the previous one).

Finally, some new refactorings can be defined to deal specifically with contracts; these include Pull Up Contract, Push Down Contract, Create Abstract Precondition, and Simplify Assertion.

In a future post I will discuss automation of contract-related refactorings and how refactoring tools can take some of the burden of the contracts.

Refactoring

Change is a way of life in software development.  Requirements change because clients gain a better understanding of their needs (possibly due to experience with an existing version of the software), to take advantage of new business opportunities, or for external reasons such as new legislation that requires new types of auditing, or change in standards.  The environment may change in various ways; for example, moving from a private data center to a public cloud, operating systems may become obsolete, or mission-specific hardware may need to be upgraded.  Change is the greatest challenge to the software development process, and development methodologies employ various tactics to accommodate it.  The classic "waterfall" methodology tries to eliminate it, by spending a lot of time in the beginning of the project trying to get the requirements just right.  Unfortunately, even if this is extraordinarily successful, by the time the other steps in the process are done, the requirements are practically guaranteed to be out of date.

Agile methodologoies take the other extreme.  Significantly, the classic introduction to Extreme Programming (nicknamed XP) by Kent Beck is called Extreme Programming Explained: Embrace Change.  These methodologies accept that change is inevitable, and gear every activity to support it.  This can only work if it is possible to modify existing software to fit changing requirements, and this is only possible if the software is always well-designed.  Unfortunately, software tends to change away from a good design, because each change is usually done without much regard for the overall design.  As changes accumulate, it becomes harder and harder to make further changes, and the likelihood of introducing errors grows in an exponential manner.  Therefore, one of the basic tenets of agile methods is that developers must take the time to restore a clean design to their software every once in a while.  This activity may seem to be unproductive, since it doesn't result in any modifications to the external behavior of the software.  However, it enables further modifications, and is therefore essential.

The activity of changing the internal structure of the software in order to restore it to a well-designed form without affecting external behavior is called refactoring.  First introduced by Bill Opdyke in his 1992 PhD thesis, and popularized in the famous book Refactoring: Improving the Design of Existing Code, refactoring is an approach to software development as well as a set of "refactorings," each of which is a detailed list of instructions on how to perform structure-modifying but behavior-preserving changes in code in a reliable way.  Reliability is achieved by performing unit tests after each small change, in an attempt to guarantee that behavior is still preserved.  If some of the tests fail, it is easy to identify the reason, since it is rooted in the last small modification performed.

Of course, in order for this to work, it is necessary to have an extensive suite of unit tests, which will guarantee (with high probability) that any change that doesn't preserve functionality will be discovered immediately.  This is easier said than done.  A good set of unit tests may be considerably larger than the production code itself, and requires significant effort to create and maintain.  Most agilists consider this to be a necessary evil; I once heard a developer say he enjoys writing these tests, and even Kent Beck, the high priest of XP, expressed his surprise at that.

Still, developing without a good suite of tests is like driving blindfolded; you can't see where you're going and you're afraid to make any change at all.  In fact, Michael Feathers, in his book Working Effectively with Legacy Code, defines a legacy system to be one for which you don't have a good suite of unit tests.  And refactoring is a very effective and satisfying way to program.  I recall several experiences in which I started making some change in my code, which led to further changes, leading to a period of several days when I couldn't even compile my code, let alone run it.  This is a terrible feeling; you know you have problems in your code, but you have no way of testing it to find out what they are.  At the end of this process, when I got back to a running system, it indeed had problems, and it took a long time to find them all and fix them.  By restructuring the work into a series of refactorings, it would have been possible to test much more often, and thus find problems and fix them much earlier.

As I said, there can be no agile methodologies without refactoring.  However, refactoring is a useful activity regardless of which methodology you use (including no methodology at all).  It does come at a cost; you must have an extensive test suite, and refactoring itself takes time and effort.  I consider this cost to be well spent, since it saves much more effort down the line, when the inevitable requirement changes appear.  Hard as it is to convince programmers to invest in their future (see Programmers as Children), this is one of the important places to try.

As in other cases, tools are a great help in following the methodology, and therefore also in convincing programmers to use it.  Furthermore, good tools take away some of the burden of checking the correctness of the transformation.  Good refactoring support exists (mostly for Java) in Eclipse and other modern IDEs, and I urge every developer to make the maximum use of these.  When I modify my code, I make every effort to use the automated refactoring capabilities provided by the IDE, as well as the related source transformations and quick fixes.  I do this even when this forces me to make the changes in a certain way or order, just to take advantage of the automation (and related reliability) in the IDE

Unfortunately, all modern IDEs have bugs in their refactoring support, chiefly due to insufficient analysis.  For example, they might create variable bindings that shadow existing bindings incorrectly.  So you must be careful when using these tools, and be aware of their limitations.  In spite of these limitations, I find them extremely useful.  One of the current research interests of our group is automating more powerful refactorings and making them more reliable; more about that in a later post.

Runtime Checking of Contracts

As I said before, the most important use of contracts is methodological; by paying attention to contracts, you will be able to avoid many errors you won't have to fix later.  Still, if you go to the trouble of writing contracts, you would like to get additional benefits.  One of the most obvious is runtime checking of contracts, which gives warning about contract violations as they occur, helping catch errors close to their sources.  Without contracts, a bug can corrupt a data structure or its contents, planting a time bomb that can explode much later.  At that point, it is difficult to discover who made the erroneous change even with a debugger, since the offending method is no longer on the stack and can't be examined, and many other traces of the buggy action may also have disappeared.

In order to get these kinds of warnings, the contract must be written in some formal language; typically it is some extension of boolean-valued expressions in the programming language.  Extensions are necessary in order to refer to "old" values; that is, allowing the postcondition to refer to values of variables or expressions on entry to the method.  Rich assertion languages also add ways of expressing universal and existential quantifiers; often, you want to express some property of all the contents of some array or other data structure, or to assert that there is some element with a given property.  However, it is easy to add such capabilities to languages that don't offer them simply by writing appropriate methods to check any required condition.

Runtime contract checking is complicated by several factors.  First is the relationship between contracts on methods in inheritance hierarchies.  As I explained in The Correct Use of Inheritance, inheriting methods may only weaken preconditions and strengthen postconditions.  There are two approaches to enforcing this constraint.  The one used by Eiffel uses syntactic enforcement, in which you can never write assertions violating this rule.  In Eiffel, overriding methods use "ensure then" instead of "ensure" for postconditions, with the meaning that any assertion following "ensure then" is conjoined with any assertions from superclasses.  For example, suppose you have a postcondition "ensure contains(x)" on the method Container.put(x); this ensures that after adding x to the container, it is indeed in it.  A list is a kind of container, and there you want to add the postcondition "ensure then count = old count + 1", which means that the number of elements in the list has increased by one after adding an element.  (This is not the case for sets, which are also containers.)  The full postcondition of List.put(x) is now "contains(x) and then count = old count + 1".  (The "and then" operator is a short-circuit operator, like && in the C family.)  Similarly, preconditions in overriding methods use "require else" rather than "require", and add the new assertions by disjunction ("or else" in Eiffel, || in the C family.)  While this approach prevents any violations of the inheritance rules, it means that you don't see the full contract in the class itself, and there could be hidden assertions you aren't aware of.  This calls for tools that can display the full contract (see Viewing Contracts).

The other approach is to require developers to maintain the correct relationships themselves, by copying assertions as necessary.  In this case, you see the full contract in each class, but need to verify for yourself that the inheritance rules hold in each case.

A runtime assertion-checking tool needs to be aware of the inherited contracts in either approach.  In the first one, it must be aware of the full contract in order to check it properly.  This is less of an issue for postconditions, because these can be checked independently.  But it is crucial for preconditions, since the fact that a precondition written with a certain overriding method is false is not an error if the precondition of the method in some superclass is satisfied.  In the second approach, assertions can be checked for each class independently, but you also want to add checks that warn in case the inheritance rules are violated.

Another complicating factor is the need to keep "old" values, as in the example shown above: "count = old count + 1".  An assertion-checking tool needs to keep the value of count on entry to the method in order to make sure that the value on exit is exactly one more.  The computation of the old value could cause an exception; for example, the Stack.put(x) method may have a postcondition "count > 1 implies item(2) = old item(1)", which means that if after insertion the stack has at least two elements, then the element that used to be on top of the stack ("old item(1)") is now second ("item(2)").  As the tool evaluates the expression item(1) on entry to the method, an exception will occur if the stack is empty.  This, however, is not an error in the program or in the assertions!  What the tool must do is keep a record of the exception, and only raise it if the old value is ever referenced.  This will never happen in this example, because if the stack was initially empty, it will have exactly one element following the put operation, the antecedent "count > 1" of the postcondition will be false, and the consequent that calls for the old value, "item(2) = old item(1)", will never be evaluated.

Yet another challenge is preventing infinite recursion in assertion checking.  For example, if the Stack class has an invariant capacity() >= 0, and this invariant is checked upon entry to the capacity method, an infinite recursion will result.  Eiffel takes a conservative view, and turns off all assertion checking while it checks any assertion.  The rationale for this is that methods used in assertions should be verified separately, before being used to specify the behavior of other parts of the program.  It is possible to check more assertions without getting into an infinite recursion, and various tools have different strategies for dealing with this issue.

Our own assertion-checking tool for Java is called Jose, and uses aspect-oriented programming to handle the issues mentioned above.  More on Jose in a later post!

Viewing Contracts

There are many ways to view a contract.  As you edit your class, you naturally see the contract for each method in the header of the method, since it is part of the text.  (In Eiffel, it is part of the syntax of the language; in design-by-contract tools for Java, the contract is typically expressed in the Javadoc comments of classes and methods.)  But what do you do when you want to see the full contract of the method, including inherited parts?  And when you are about to call some method of another class, how do you know what is the full contact for that method?

The contract can have private parts, which are not meaningful to clients.  As I mentioned previously, preconditions must be fully understandable to clients, since otherwise they can't be expected to comply with them.  However, postconditions and invariants may refer to private parts of the implementation.  For example, suppose your Queue class uses a circular buffer, called items, to implement the (bounded) queue.  The implementation invariant should specify that items != null.  This is an important property of the class to its implementer and anyone creating an inheriting class, but it shouldn't be exposed to clients who aren't supposed to know about implementation details.  Similarly, the method that adds an element to the queue may have a postcondition specifying that the write-pointer has advanced by 1 modulo the buffer size.  Again, this is useful information to the implementer, but should be hidden from clients.

The distinction between private and public access levels, in code or in contracts, is usually not clear cut.  For example, Java provides four different access levels; C++ has three, but allows "friends" to access private and protected members; and Eiffel has a selective export mechanism where a class can specify which other classes have access to each of its features.  This means that the same class can present different interfaces to other classes, depending on their access levels.  As always, interfaces include the methods visible to the particular client, as well as the contract.  Different parts of the postconditions and invariants of the contract would be visible to different clients.

The Eiffel development environment can show contracts in different ways, based on whether to show private assertions or not, and whether to show assertions from a single class or show all inherited assertions as well.  However, the views can't be customized by client.  I don't know of any other development environment that can show more than one view of a contract.  Ideally, the environment would be able to show contracts from a supplier's perspective as well as from the perspective of any client.  For example, if I'm editing class A, and place the cursor on a call to a method f of class B, I should be able to see (in a tooltip or in a separate view) the full contract of B.f from the point of view of class A.  Such a view is not difficult to create, although it might require some tedious work.  I consider such a view essential to any development environment that takes design-by-contract seriously.