# Inverting Maps in Dafny

I had cause to need to prove some things about injective maps and inverses.

 // union on maps does not seem to be defined in Dafny function union(m: map, m': map): map requires m !! m'; // disjoint ensures forall i :: i in union(m, m') <==> i in m || i in m'; ensures forall i :: i in m ==> union(m, m')[i] == m[i]; ensures forall i :: i in m' ==> union(m, m')[i] == m'[i]; { map i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i] }   // the domain of a map is the set of its keys function domain(m: map) : set ensures domain(m) == set u : U | u in m :: u; ensures forall u :: u in domain(m) ==> u in m; { set u : U | u in m :: u }   // the domain of a map is the set of its values function range(m: map) : set ensures range(m) == set u : U | u in m :: m[u]; ensures forall v :: v in range(m) ==> exists u :: u in m && m[u] == v; { set u : U | u in m :: m[u] }   // here a map m is smaller than m' if the domain of m is smaller than // the domain of m', and every key mapped in m' is mapped to the same // value that it is in m. predicate mapSmaller(m: map, m': map) ensures mapSmaller(m,m') ==> (forall u :: u in domain(m) ==> u in domain(m')); { forall a :: a in m ==> a in m' && m[a] == m'[a] }   // map m is the inverse of m' if for every key->value in m // there is value->key in m', and vice versa predicate mapsAreInverse(m: map, m': map) { (forall a :: a in m ==> m[a] in m' && m'[m[a]] == a) && (forall a :: a in m' ==> m'[a] in m && m[m'[a]] == a) }   // map m is injective if no two keys map to the same value predicate mapInjective(m: map) { forall a,b :: a in m && b in m ==> a != b ==> m[a] != m[b] }   // here we prove that injective map m has an inverse, we prove // this by calculating the inverse for an arbitrary injective map. // maps are finite in Dafny so we have no termination problem lemma invertMap(m: map) returns (m': map) requires mapInjective(m); ensures mapsAreInverse(m,m'); { var R := m; // part of m left to invert var S := map[]; // part of m already inverted var I := map[]; // inverted S   while R != map[] // while something left to invert decreases R; // each loop iteration makes R smaller invariant mapSmaller(R, m); invariant mapSmaller(S, m); invariant R !! S; // disjoint invariant m == union(R, S); invariant mapsAreInverse(S,I); { var a :| a in R; // take something arbitrary in R var v := R[a]; var r := map i | i in R && i != a :: R[i]; // remove a from R I := I[v:=a]; S := S[a:=v]; R := r; } m' := I; // R is empty, S == m, I inverts S }   // here we prove that every injective map has an inverse lemma injectiveMapHasInverse(m: map) requires mapInjective(m); ensures exists m' :: mapsAreInverse(m, m'); { var m' := invertMap(m); }   // here we prove that no non-injective map has an inverse lemma nonInjectiveMapHasNoInverse(m: map) requires !mapInjective(m); ensures !(exists m' :: mapsAreInverse(m, m')); { }   // here we prove that if m' is the inverse of m, then the domain of m // is the range of m', and vice versa lemma invertingMapSwapsDomainAndRange(m: map, m': map) requires mapsAreInverse(m, m'); ensures domain(m) == range(m') && domain(m') == range(m); { }   // a map m strictly smaller than map m' has fewer elements in its domain lemma strictlySmallerMapHasFewerElementsInItsDomain(m: map, m': map) requires mapSmaller(m,m') && m != m'; ensures domain(m') - domain(m) != {}; { var R,R' := m,m'; while R != map[] decreases R; invariant mapSmaller(R,R'); invariant R != R'; { var a :| a in R && a in R'; var v := R[a];   var r := map i | i in R && i != a :: R[i]; var r' := map i | i in R' && i != a :: R'[i];   R := r; R' := r'; } assert R == map[]; assert R' != map[];   assert domain(R) == {}; assert domain(R') != {}; }   function invert(m:map) : map requires mapInjective(m); ensures mapsAreInverse(m,invert(m)); { injectiveMapHasInverse(m);   var m' :| mapsAreInverse(m,m'); m' }

# Incremental software projects can be less risky

Inability to proceed incrementally is risk factor for project failure. If you have to wait until the end of the project for delivery, then you get (or don’t get) all your features at that point. What if an unexpected event occurs? Then you may reach the project end date still with all features in progress and none finished!

How does this problem manifest? You have a big list of features that are partially working, or “in progress”, and few features that are “finished” or “not started”. Perhaps you have even lost track of which features are finished or not, or how completed the features are, or how completed the project is?

What I prefer to see in a de-risked project is: a list of completed features; one in-progress item that is currently being worked on; and a bunch of not-started-at-all items. It can be risky to have a process of “filling-in” the code from a sort of sketch implementation across all of the features – I generally prefer an incremental process of adding features one-by-one to a known finished and working base. If you need to check on features to inform the design process then implement simple, but complete, minimal versions of the key features. But do them one at a time.

The three main problem with lots of started-but-not-finished items are:

1. that it can be difficult to understand how much work actually needs to be done before you get any further completed features, there is a /risk/ that big surprises can come up late on.
2. that it is difficult for testers to give you early feedback on the quality of your implementation – they end up having to test all the features at the end. And at the end is when you have no time left to fix any problems they may discover. Of course they may not discover any problems, but I am talking about risk management and predictability.
3. and if you do get your testers going early then they don’t know if something they don’t like about the product is caused by an incomplete feature, or is a genuine problem. You can end up with lots of wasted time for testers and developers as they try and sort this communication problem out. And I think it can lead to testers getting used to a lower quality of half-finished software.

There are more problems actually, but those are the most serious ones in the short term. Maybe I will write more about this later.

# Blog Review: Should I comment code?

I want to try to get a sense of the set of reasons that people have for commenting or not commenting code. What follows is a table of blog posts (and similar) with an assesment of if they are generally for or against comments in code, and extracts which (I think) give an overview of their key points.

If you have any more links (perhaps something you have written) then please feel free to add them in a similar format in the comments on this post.

Post Position  Comment
The Hows and Whys of Commenting C and C++ Code Pro Comments should reveal the underlying structure of the code, not the surface details. A more meaningful comment would be “int callCount = 0; //holds number of calls to [function].”
Why comments in code are largely pointless Anti as we do the standard stuff we comment the code frequently and with confidence […] when it comes to something a bit more difficult we maybe have to try a few different options before we get it right […] there is little imperative to go back and document your work […] you get a large amount of commentary on the pedestrian every day part of your application and very little in the more interesting areas
Commenting Code Effectively: The How AND The Why Pro “why was it done that way in the first place?” […] Much like a math teacher asks you to show your work so that they can see how you arrived at the answer, a developer must comment their code as they are writing it to document (1) how the code works, and (2) why it was written that way. The developers thoughts and decisions are just as important in the comments as an explanation of how the code works. […] Make sure all methods and parameters are documented, explaining what is the purpose of each method and what are the expected parameters and results
The Problem With Comments Pro Comments should be displayed in the UI by editors as more important than the code (e.g. in bright colors)
Why would company develop an atmosphere which discourage code comments? forum
Comments are a code smell forum on balance probably pro
Eliminating Comments: the Road to Clarity Anti It is not that comments in and of themselves are bad. It’s more that having comments in your code indicates that your code itself is not clear enough to express its intent.
Common Excuses Used To Comment Code and What To Do About Them Anti (extensive extracts as post is no-longer available) Just two years ago, I was beyond skeptical towards the forces telling me that comments are worse-than-useless, self-injuring blocks of unexecutable text in a program. I thought the idea was downright ludicrous. But as I’ve made an effort towards reaching this nirvana called “self-documenting code,” I’ve noticed it’s far more than a pipe dream. […] you can choose better variable names and keep all code in a method at the same level of abstraction to make is easy to read without comments. […] want to keep track of who changed what and when it was changed. Version control does this quite well […] The code too complex to understand without comments. I used to think this case was a lot more common than it really is. But truthfully, it is extremely rare. Your code is probably just bad, and hard to understand. […] Natural language is easier to read than code. But it’s not as precise.
Don’t Comment Your Code Anti In the vast majority of cases, a comment indicates that something is wrong. If you have to add a comment to explain what a block of code is doing, that means that the code is too complicated or is using poor variable names or function calls.
Not Commenting And The Tipping Point Of Poor Programming Not Sure It’s one thing for a person, such as Brian, that writes very high quality code, to keep his comments to a minimum. But what about the majority of people who are not at his level? These are people who are not writing great code to begin with – are they going to view these blog posts as the excuse and justification to stop commenting their code? What happens then? We have an epidemic (as Gladwell would put it) of poorly written and poorly commented code. […] I am merely trying to play devil’s advocate to keep things in perspective.
Code Tells You How, Comments Tell You Why Anti/Caveat If you write your code to be consumed by other programmers first, and by the compiler second, you may find the need for additional comments to be greatly reduced. […] [code] can’t explain why the program is being written, and the rationale for choosing this or that method. [code] cannot discuss the reasons certain alternative approaches were taken.
Why programmers don’t comment their code Pro That’s probably not true unless you wrote it in COBOL. You may very well know that
\$string = join(”,reverse(split(”,\$string)));
just reverses your string, but how hard is it to insert
# Reverse the string
Why not to comment code Anti Every time you’re tempted to comment, take the time to think if you can make the code tell its own story, e.g., instead of some branching condition, extract the condition into a method to emphasize the story of why over how.
Developers comment to explain a confusing part of their code rather than take the time to refactor it by extracting a method or naming a variable properly. Inevitably the code gets modified and the comment rots.
On Commenting Source Code – Why Commenting is Not Bad Practice Pro Maybe I’m missing something, but that’s not how I see the purpose of refactoring. When I refactor code I don’t arbitrarily break out larger functions into smaller functions that are only ever called once. Instead, I look for patterns that are repeated across the code base and try to create new functions that encapsulate those patterns.
Portrait of a N00b Unknown (couldn’t understand this post, a bit TL;DR combined with it somehow being a long missive on static types and if they are like comments or not) Should a team write for the least common denominator? And if so, exactly how compressed should they make the code? I think the question may be unanswerable […] I think the general answer to this is: when in doubt, don’t model it. Just get the code written, make forward progress. Don’t let yourself get bogged down with the details of modeling a helper class that you’re creating for documentation purposes.
comments are a sign of bad code and I am not sorry for saying it Anti Comments are not bad, the code is – I’m not suggesting to forgo the use of comments, but that they are only band-aids. […] Code should not be written to the level of the dumbest developer, the dumbest developer should be brought to the level of the code (though I want to reiterate good code should be easily readable).
How bad comments are born in your code Pro I don’t think going to the extreme and having comments replaced with just relevant class/method naming is a good idea because you cannot express full intent in a class/method name. This is actually why you have to write some code inside the class or the method, isn’t it? […] To summarize with only one word the reason for commenting code is maintenance!
Code commenting? Try Business Commenting. Pro one thing I rarely hear mentioned is that it’s often more interesting to comment the business justification than it is to comment the code. Jeff goes some way towards suggesting this when he says to comment the “why”, but for many people that translates to “Why did I write the code this way?”. I often find that code I’m maintaining is missing comments regarding the business logic. Rather than “Why is the code designed like this?”, something like “Why is the business process designed like this?”
Once Again: Comments In Code Aren’t Necessarily Bad Pro/Caveat I generally agree that you should strive to avoid comments in code. That is, you should write your code in a way that doesn’t require comments for the reader to easily understand and grasp what the code is doing. However… there are situations where comments are helpful (or even required) […] That code applies a certain pattern which isn’t well known, but there is a very specific reason why the pattern is needed. And I still believe that most developers need comments to understand it properly. […] if you need to write some code in a very non-obvious way, then you could really make things easier for those who need to maintain it […] by including some comments to explain why a certain solution/pattern was chosen.
Cleaning bad code Anti Even when comments are correct and useful, remember that you will be doing a lot of refactoring of the code. The comments may no longer be correct when you are done. And there is no unit test in world that can tell you if you have “broken the comments”. Good code needs few comments because the code itself is clearly written and easy to understand. Variables with good names do not need comments explaining their purpose. Functions with clear inputs and outputs and no special cases or gotchas require little explanation. Simple, well written algorithms can be understood without comments. Asserts document expectations and preconditions.
Don’t comment bad code—rewrite it. Forum
what makes beautiful code Anti Comments are code smells
Don’t comment your code! Anti it’s way harder to write good comments then no comments at all. So instead of making it all worse just don’t do it. If you consider yourself as someone who writes exceptable code, that should explain enough for you and your co-workers.
Should you comment your code? Pro Assuming that your code is good enough to not require any comments is very egostical. What is perfectly clear and logical to you because you have been working on a system for a couple of years will not be clear to someone who is new to the system. Put another way, code tells you how something is done and comments tell you why.

# Alternative distance function for Stable Abstractions Principle

Tools such as STAN use a distance function D = A + I – 1 to measure how well a particular package meets the stable-abstractions design principle. In my opinion this measure includes a lot of points in the design space that are not good places. Specifically, I think that packages should fall into the upper left or lower right corners only. This is particularly importaint if we consider the distance function to be a cost function and we are trying to automatically search for good designs. The D function can produces packages that are half abstract and half stable, which I would prefer to avoid.

Instead I propose to use the normalised absolute difference in the distance from the two desirable corners of the design space. Specifically I favour designs which are closer to either the stable-abstract or unstable-concrete corners of the design space, over designs which happen to be near the “main sequence” but are further from the desirable corner. I propose the distance function D’=sqrt(2) – abs(sqrt((1-I)**2 + A**2) – sqrt(I**2 + (1-A)**2))/sqrt(2). This function weighs the desirable corners the highest and provides a watershed so that a search function can converge towards the most desirable part of the design space by cost-minimisation.

Proposed stable-abstractions distance function (D’):

For comparison the original stable-abstractions distance function (D):

To make the difference bettween these two functions concrete: here is a plot of the absolute difference between the functions. The red areas are the areas of most aggreement. You can see that the central disputed area is the area of the design space most affected by the selection of my proposed new function, positive figures are less favoured areas in the proposed D’ function.

# Avoiding the Dependency Injection Facebook Problem

Last year Steve Freeman published a blog article describing how the use of dependency injection could lead to coupling between objects that should have no knowledge of each other. The essential idea is that using dependency injection uniformly for all relationships between objects within the program makes it harder to understand and control the higher level structure of the program; you turn your program into an unstructured bag of objects where every object can potentially talk to every other object.

I thought that I would write a bit about my approach to dealing with this problem in Java programs: how I try to add higher level structure to the code; and how I use the tools to enforce this structure. I am going to take a long diversion through the practices I use to organise Java code before I talk about Dependency Injection. If you want to only read that bit, then skip to the end.

The following are my versions of the diagrams from a post about the problem with DI frameworks by David Peterson. I start with the same unstructured graph of objects and use the same basic progression in order to describe how I use the Java programming language to resolve these issues without having to sacrifice the use of my DI framework (should I want to use one).

For the sake of argument, the program begins as an unstructured graph of objects dumped into a single package within a single component (or project). The objects are all compiled together in one instantiation of the Java compiler. This program is likely to be quite difficult to understand and modify – not least, where do you even start trying to understand it? We can do better.

Types, Packages and the Classpath are the ways that the Java programming language offers compiler support for organising code into higher level abstractions. The benefit of using packages is that the compiler type system will enforce the abstraction boundary. If a type definition is marked as package visible then no code outside the package with a reference to such a type (class or interface name) will compile.

I refactor the code by identifying a related sets of classes and moving them into a package. Without breaking the program I then mark every type that I can as package visible. Now I can see some of the structure of my code: I can see which classes are implementation details of a particular abstraction; and I can see what protocol each of my abstractions provides by looking at its public classes. I cannot accidentally depend on an implementation detail of my abstraction because the Java compiler will prevent me (provided I have defined sufficient types and don’t do too much reflection).

There might be a lot of packages involved in a realistic program so I would like another level of abstraction that I can use to organise my packages into groups of related packages. I do this by organising my packages into libraries. All of the packages in my library will be compiled together in one single instantiation of the compiler, but each of my libraries will be compiled separately. I want to detect any accidental dependencies between my libraries so I will only put the minimum necessary libraries onto the classpath of each invocation of the compiler.

I can now see the high level component organisation of my program and I can see which components are used by a given component. I may even be able to see which component is the entry point of my program – the entry point component will transitively depend on all the other components. There are still two further properties I would like my code to have: I do not want to accidentally create a dependency between a package in one library and a package in another library (its public protocol should be clearly defined); and I would like the entry point of the application to be immediately obvious (so a code reader can start reading with no delay).

I extract the public interface of my library into a new library, and change the users of that library to depend only on the public interface. I also replace the implementation jar with the new API-only jar on the compiler classpath anywhere it occurs in my other libraries. This is a form of dependency inversion. The new interface library cleanly describes the protocol provided by the implementation and the separate compilation ensures that users of the library only depend on the public protocol.

I then extract the entry point (the highest level wiring) of the program into its own component. This component contains the minimum code necessary to instantiate the top level components, wire them together and start the execution. This is a form of inversion of control.

The structure of my program is now not only represented in the organisation of the code, but the structure is also enforced by the Java compiler.

I can looking at the package structure of the code.

Or I can look at the component structure of the code.

What structure am I now able to obtain from the code?

• Package API – by looking at the visibility of my classes
• Package Relationships – by looking at the packages in each library
• Library API – by looking at the fully abstract library component
• Library Relationships – by looking at the classpath of each library
• Program high-level organisation – by looking at the classpath of each library and the entry-point wiring

## Dependency Injection and Dependency Injection Frameworks

So why haven’t I mentioned Dependency Injection and Dependency Injection frameworks? And how does all this relate to the “Facebook Dependency Injection” problem?

I can now choose to use dependency injection as much or as little as I want/need to. If I want to inject one library into another, or inject one package into another then I can just provide an appropriate factory. If I want to use new, I can do that too. The use of package or public visibility will distinguish between the peer objects and the internal implementation details. The Java compiler will prevent me from creating any unwanted dependencies by enforcing package protection. The same argument applies to dependencies between libraries: I can distinguish the public API of the library by splitting it out; by only having the public API on the classpath I can be sure that I will not accidentally use an implementation detail of a dependency.

The type system and compiler will help me prove to myself that the program will only instantiate an object graph with the structure that I intended.

I am now free to use a Dependency Injection framework anywhere within my code that I feel it is appropriate. I can use a Dependency Injection framework to wire up the implementation classes of a package, I can use it to wire up the packages of a library or I can use it to wire together my libraries – or any combination I choose. I can even use a different Dependency Injection framework within each of my libraries or even within each of my packages if for some reason I need to do that! I can be sure the structure of my program doesn’t just become a bag of objects because the compiler enforces it for me – I cannot just pull in an object of any type into my object, I can only pull in an object that has a type that is in the the public API of a library (and package) that is on my classpath.

# What is the Java type system for? – Case coverage

So what might a programming language with strong static named types be useful for? I recently asked an interview question about how the observer pattern could be implemented in a situation involving the occurrence of a number of different types of events. This answer was suggested:

 interface EventListener { void eventOccurred(Event event); }   class MyEventHandler implements EventListener { void eventOccurred(Event event) { if(event.getType() == EventType.subtypeOne) { doTypeOneThing((EventSubtypeOne) event); } else if(event.getType() == EventType.subtypeTwo){ doTypeTwoThing((EventSubtypeTwo) event); } else { throw new RuntimeException(); } } }

There are a number of issues with this design, however the main issues that occurs in the kind of large programs I often work on is: when a new type is added how do you make sure that all of the types of events are handled in every implementation of EventListener?

The suggested solutions are often along the lines of writing test cases for each of your EventListener implementations and taking the absence of an exception as success. But then how do you make sure you have updated all of your tests correctly?

A simple, easy to understand, and Object Orientated way to resolve this problem is:

 interface EventListener { void eventOneOccurred(EventOne event); void eventTwoOccurred(EventTwo event) }   class MyEventHandler implements EventListener { void eventOneOccurred(EventOne event) { doTypeOneThing(event); }   void eventTwoOccurred(EventTwo event) { doTypeTwoThing(event); } }

1. No casting. Since we never represent the event as a generalised abstraction, we never need to downcast the event. We don’t even need a base type for event unless we have some use for that abstraction in our system.
2. No runtime error. As long as all the code is compiled together (or at least has binary compatibility) then no runtime error will occur because our type system proves that all the types of events are handled.
3. Updates are easy. When we add a new event type, we add the new method to the interface and the compiler will tell us where all the implementations are! This is very fast if you have an IDE with incremental compilation and all the code. But it will work safely even in situations where the people implementing your interfaces are distributed and you have no possibility of updating their code. When they try to compile against the new version of your library they will immediately find out about the new feature (if they like it or not)!

Of course, you don’t always want these properties in every design. But when you do want your design to have these properties, this is how you can do it.

# JewelCli accessor method names

JewelCli 0.8.2 and above supports query methods with or without the “get” prefix:

 public interface MyExample { @Option String getMyOption();   @Option String myOtherOption(); }

The instance strategy now supports mutators with or without the “set” prefix:

 public class MyExample { @Option void setMyOption(String value) {}   @Option void myOtherOption(String value) {} }

# How are REST APIs versioned?

I am currently working on a REST API, and the question was raised, how are, and how should, REST APIs be versioned? Here are the results of my research.

It seems that there are a number of people recommending using Content-Negotiation (the HTTP “Accept:” header) for API versioning. However, none of the big public REST APIs I have looked at seem to be using this approach. They almost exclusively put the API version number in the URI, with the odd exception using a custom HTTP header. I am at somewhat of a loss to explain this disconnect.

## Versioning strategies in discussions

Post Versioning
Stack Overflow 1 URI
Stack Overflow 2 Content Negotiation
blog post by Jeremy Content Negotiation
ycombinator discussion some opinions both ways
Stack Overflow 3 Content Negotiation
Stack Overflow 4 Content Negotiation
notmessenger blog post URI (against all headers)
Peter Williams Content Negotiation (strongly against URIs)
Apigee Blog post on API versioning URI (some discussion)
Mark Nottingham REST versioning Recommending essentially versionless extensibility with a HATEOS approach
Nick Berardi on REST versioning URI
Tom Maguire on REST versioning Content Negotiation
Nicholas Zakas on Rest Versioning URI
Steve Klabnik on Rest Versioning Content Negotiation + HATEOS
Luis Rei on Rest Versioning Content Negotiation with (;version=1.0)
kohana forum discussion on REST versioning Many Opinions
Troy Hunt on REST versioning Accept Header but also support custom header and URL
Paul Gear REST versioning Recommending essentially versionless extensibility with a HATEOS approach

## Versioning strategies in popular REST APIs

API Name Versioning Example
Twillo date in URI
Atlassian URI
Github API URI/Media Type in v3 Intention is to remove versioning in favour of hypermedia – current application/vnd.github.v3
Bing Maps URI
Netflix URI parameter http://api.netflix.com/catalog/titles/series/70023522?v=1.5
Salesforce URI with version introspection {
“label”:”Winter ’10”
“version”:”20.0″,
“url”:”/services/data/v20.0″,
}
Flickr No versioning?
Digg URI http://services.digg.com/2.0/comment.bury
Delicious URI https://api.del.icio.us/v1/posts/update
Last FM URI http://ws.audioscrobbler.com/2.0/
Foursquare URI https://api.foursquare.com/v2/venues/40a55d80f964a52020f31ee3?oauth_token=XXX&v=YYYYMMDD
paypal parameter &VERSION=XX.0
Etsy URI http://openapi.etsy.com/v2
Tropo URI https://api.tropo.com/1.0/sessions
Tumblr URI api.tumblr.com/v2/user/
openstreetmap URI and response body http://server/api/0.6/changeset/create
Ebay URI (I think) http://open.api.ebay.com/shopping?version=713
Reddit No versioning?
Groupon URI http://api.groupon.com/v2/channels//deals{.json|.xml}
Geonames
Wikipedia no versioning I think?
Bitly URI https://api-ssl.bitly.com/v3/shorten
Disqus URI https://disqus.com/api/3.0/posts/remove.json
Yammer URI /api/v1
Drop Box URI https://api.dropbox.com/1/oauth/request_token
Amazon Simple Queue Service (Soap) URI Parameter and WSDL URI &Version=2011-10-01

## Versioning strategies in popular REST Libraries

Library Name Versioning Example
node-restify semver versioning in an accept-Version header accept-version: ~3
Jersey description of how to do Accept: header versioning in Jersey Accept: application/vnd.musicstore-v1+json

# JewelCli Constrained Multivalued Option

A new feature in JewelCli 0.8.1 is the ability to constrain the multiplicity of multivalued options. If the arguments given by the user do not match the constraints an appropriate ArgumentValidationException is thrown.

### Minimum

 public interface ListWithMinimumOfOne { @Option(minimum = 1) List getMyOption(); }

### Maximum

 public interface ListWithMaximumOfFour { @Option(maximum = 4) List getMyOption(); }

### Exact Count

 public interface ListWithExactlyThree { @Option(exactly = 3) List getMyOption(); }

# JewelCli Hidden Options

As of version 0.8.1 JewelCli supports hidden options. These are options that will not show up in your help message.

 interface HiddenOptionNotIncludedInHelp { @Option(hidden = true) boolean getDebug(); }

Will create an option called “–debug” which you can specify on the command line, but will not be advertised in any help messages.