Consider use of functions as well?

[KantarBruceAdams]

Hi,
I have been looking for DBC support for go as well. I like your approach of ensuring that the generated code agrees with the documentation. I wonder if we could have the best of both worlds if you generated code that used functions to implement the contract as per https://godoc.org/github.com/lpabon/godbc?

Personally I want to assert pre-conditions in production but not post-conditions (which are often hard to compute and covered by extensive unit tests.
I also want to document all my pre-conditions , post-condiions and invariants even those that are hard to compute.
Coming from C++ I used doxygen for DBC commenting, an assertion macro for pre-conditions and unit tests for post-conditions and invariants. Generating a contract checking wrapper to a function would be very useful in the testing context.

The ultimate DBC package to me, might allow:

• just checking that pre-conditions, post-conditions and invariants in the code and documentation match
• generating checks from documentation - as you do now
• generating documentation from checks - the inverse - which I presume is not done
• allowing documented checks which are not generated
  e.g. "foobar() must have been invoked first to setup the snafu"

I would like to propose a minimum change towards this goal of:

• allowing documented checks which are not generated
• using functions for the generated checks (like https://godoc.org/github.com/lpabon/godbc)
  so that your package is still usable/preferable even if the code generation part is not used.

I presume this package overwrites generated contracts rather than "checking that pre-conditions, post-conditions and invariants in the code and documentation match" which is a harder problem but please correct me if I am wrong.

What is the current behaviour if code for a check cannot be generated?
Is this left to be picked up as a build failure downstream?

Regards,

Bruce.

[KantarBruceAdams]

On a related note you depend on the godoc syntax specification but I cannot find one - https://stackoverflow.com/questions/53101458/where-is-the-specification-for-godoc-itslef

[mristin]

Hi @KantarBruceAdams
Thanks a lot for your feedback!

I identify three points in your message, please correct me if I'm wrong:
a) missing invariants
b) toggling of contracts (keeping some in the code during the production, while keeping others during testing)
c) contracts from code (reverse-contracting)

Invariants. So far, we had very little feedback on people using gocontracts, so I didn't look into the issue. I created an issue on github just right now for further discussion: #25

Toggling contracts. This is actually already possible with gocontracts. You can create two files that define the same constant (say InProd) with different build directives (//+build prod and //+build !prod) where you set it to false in the one file and to true in the other, respectively. Godbc follows the same approach.

Then you need to include that file in all the files where you define contracts and include it in the conditions (as InProd && ...). The go compiler will automatically optimize away the contract code if the constant was set to false.

I would suggest you to introduce one build tag per package or per library (whatever seems like a better fit), so that the users of your code can decide the granularity of the contracts applied, e.g., when they are performing integration testing against your code.

An additional benefit of this approach is that you explicitly document when your contracts apply so that the users of the library can double-check themselves if the contracts are verified or not (and if not, why not).

Please let me know if that didn't / doesn't work for you and what the concrete blockers are.

Reverse-contracting. This seemed to us like a too difficult task akin to a tar pit 😄 I think there would be too many edge cases which needed to be covered that it would sap a lot of energy to implement, while we couldn't identify a clear use case in our code base.

Regarding godoc syntax: could you please clarify a bit? What do you mean by it? There is this blog post: https://blog.golang.org/godoc-documenting-go-code (you already mentioned it in the stackoverflow question.)

[mristin]

Hi @KantarBruceAdams
I added a subsection to the Readme that should explain in a bit more detail how to toggle the contracts: https://github.com/Parquery/gocontracts#toggling-contracts

Please let me know if the text is clear enough.

[KantarBruceAdams]

Actually the main point of this:

• I wonder if we could have the best of both worlds if you generated code that used functions to implement the contract as per https://godoc.org/github.com/lpabon/godbc?
  For example. For "len(args) >= 1" Instead of generating:

  // Pre-condition
  if !(len(args) >= 1) {
  panic("Violated: len(args) >= 1")
  }

You could generate:

// pre-conditions
godbc.Require(len(args) >= 1, "Violated: len(args) >= 1")

But I subverted my own thread.
Here I am using github.com/lpabon/godbc but you could provide something yourself or make it hookable.
The advantage of this would be.

1. you can use your library instead of godbc to hand write contract enforcement code
2. code implementing contracts is obvious even without the comment blocks (and potentially machine modifiable)

At the moment it is hard to mix gocontracts with godbc.

[mristin]

Hi @KantarBruceAdams,
Could you please clarify a bit the benefit of having a separate function?

I see it actually as beneficial to dispense of a function call: the contract checking code is explicit and directly readable, while the constants in the conditions allow you to easily track in which situations the contract is verified (or not). Moreover, the constant boolean in the condition allows for arbitrary granularity of contract toggling, while the function from an external library imposes the granularity on the caller.

[KantarBruceAdams]

For me there are several benefits:

• Its very obvious that something is part of a contract both to a machine and a human
• You can change the behaviour of contracts without modifying the code at the point of the contract
  (e.g. log, exit, ignore)
  a panic might not always be the best option.

If you want arbitrary granularity of contract toggling I don't think the condition is perfect.
"If (condition or enabled)" might confuse some people into thinking the enabled part is part of the contract .
You can still have granularity at the calling site with a separate optional parameter to the function
E.g.
godbc.Require(len(args) >= 1, "Violated: len(args) >= 1", enabled)

Another thing is I don't like having to repeat the condition in the message.
For the equivalent in C or C++ the condition expression can be stringised in a macro. I'm not how to do that in go. You need to pass the expression to the contract checker function rather than the result of evaluating it instead. One part of the function would stringify it if evaluation failed.

[mristin]

Hi @KantarBruceAdams ,
We implemented all these features (conditions as decorators and informative violation messages generated from the condition code) in our Python contract library (https://github.com/Parquery/icontract/).

However, Go does not support such an approach: there are no macros and you don't even have optional arguments. That's why we implemented gocontracts in the first place: so that you define conditions only once, and you read them in the violation message automatically.

Its very obvious that something is part of a contract both to a machine and a human

Could you please make an example? I fail to see how these two code snippets are different to read:

// SomeFunc does something.
//
// SomeFunc requires:
//  * x > 0
//  * x < 100
//  * some condition: y > 3
//
// SomeFunc ensures:
//  * strings.HasPrefix(result, "hello")
//
// Some text here.
func SomeFunc(x int, y int) (result string, err error) {
	// Pre-conditions
	switch {
	case !(x > 0):
		panic("Violated: x > 0")
	case !(x < 100):
		panic("Violated: x < 100")
	case !(y > 3):
		panic("Violated: some condition: y > 3")
	default:
		// Pass
	}

	// Post-condition
	defer func() {
		if !(strings.HasPrefix(result, "hello")) {
			panic("Violated: strings.HasPrefix(result, \"hello\")")
		}
	}();  // some comment here

	return
}

and:

// SomeFunc does something.
//
// SomeFunc requires:
//  * x > 0
//  * x < 100
//  * some condition: y > 3
//
// SomeFunc ensures:
//  * strings.HasPrefix(result, "hello")
//
// Some text here.
func SomeFunc(x int, y int) (result string, err error) {
	// Pre-conditions
	godbc.Require(x > 0, "Violated: x > 0")
	godbc.Require(x < 100, "Violated: x < 100")
	godbc.Require(y > 3, "Violated: some condition: y > 3")

	// Post-condition
	defer func() {
		godbc.Ensure(strings.HasPrefix(result, "hello"),
			"Violated: strings.HasPrefix(result, \"hello\")")
	}();  // some comment here

	return
}

The machine can't access contracts in real time in neither of the snippets. Function calls are marginally shorter, but then the reader might not realize that they panic.

I see the only real benefit of the function approach when the user of the gocontracts can specify individually her dbc module and then choose which assertion library to use. But this is such a marginal benefit to me (and rather confusing to folks who read the code) that I decided against it.

[KantarBruceAdams]

I have left an honourable mention of gocontracts in regards to discussions about attributes/annotations in go. C++20 includes contracts as attributes

[mristin]

Thanks! I'll keep an eye on it. It would be so much better if they integrated DbC in the language.

[mristin]

Hi @KantarBruceAdams,
I've just added the support for contract preamble, so that you can use whatever library you want to assert the contracts (including godbc). For example:

import "github.com/lpabon/godbc"

// SomeFunc does something.
//
// SomeFunc preamble:
//	godbc.Require(x > 0, "x positive")
//	godbc.Require(x < 100, "x not too large")
func SomeFunc(x int) {
	// Preamble
	godbc.Require(x > 0, "x positive")
	godbc.Require(x < 100, "x not too large")

	// function body ...
}

Could you please let me know if this resolves your issue?