Skip to content

More Robust GSL Contracts #1156

Open
Open
@suncho

Description

@suncho

I was looking at the Microsoft GSL implementation of the Expects and Ensures macros to see how they worked and I discovered that they both do exactly the same thing:

https://github.com/Microsoft/GSL/blob/master/include/gsl/gsl_assert

The behavior I had expected was that the Ensures condition would be evaluated when the block exited. Instead, it's just an on-the-spot assert. This means that to properly use Ensures, you have to slap an Ensures statement at every possible exit point of your function.

So I decided to fix it and implement the behavior I had expected in the first place:

https://github.com/suncho/GSL/blob/c9ecdfcbc170a75b666d8ba42fd7fed5e58df380/include/gsl/gsl_assert

With this implementation, you can now put your Ensures statement at the top of your function body and it will automatically check that the condition is met when the function exits. I also implemented AlwaysEnsures to do the check even if the function exits via exception.

Because some functions simply maintain invariants, expressing that would require Expects and Ensures statements for the same condition. So I also added a Maintains macro and an AlwaysMaintains macro to express that invariants are maintained. These macros aren't strictly necessary, but they seemed like obvious additions because they simplify readability and reduce the chance of bugs that may arise from having to specify the same condition twice.

I had submitted a pull request to the MS GSL implementation, but @neilmacintosh suggested that I raise the issue here first:

microsoft/GSL#637

He was worried that my implementation didn't match up with the description in the Core Guidelines. Is there any reason why it shouldn't?

If you had been putting Ensures at the end of your function bodies, my implementation should still work the same as the old version.

I think the only time the behavior would change is if you had code where you used Ensures to check a condition and then changed the condition after the Ensures, but before the end of the block. In that case, you weren't properly using Ensures to check post-conditions anyway.

Metadata

Metadata

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions