Dafny precondition checks in generated code

I was wondering if there is a way to add precondition checks in the Dafny generated code. For example, let's take the following code snippet:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   requires 0 < y
   ensures less < x < more
{
   more := x + y;
   less := x - y;
}

I'd like that the resulting code in C++ to have the following check:

assert(0 < y);

If this is not available in Dafny, what options do I have? Thank you!

There is no automatic way to turn the requires clause into a run-time check. The condition of a requires clause is in a ghost context, so it may not be compilable in general. Also, if you verify your program, then you know the condition is always going to evaluate to true, so there's no point in also checking it at run time.

To support situations where the condition to be checked is too difficult to verify statically, and especially to support cross-language situations where the caller is not written in Dafny and therefore not verified, Dafny has expect statements. You can use expect in your example to trade the statically verified precondition for a run-time check:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   ensures less < x < more
{
   RuntimeRequires(0 < y);
   more := x + y;
   less := x - y;
}

method RuntimeRequires(cond: bool)
   ensures cond
{
   expect cond, "precondition failure";
}

Note that without the requires clause, you will not get any static verification at call sites.

As one other variation, you could use both a requires clause and the RuntimeRequires method I showed. If you do, I would suggest you change the specification of RuntimeRequires from an ensures to a requires, to make sure you have copied the condition correctly.

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   requires 0 < y
   ensures less < x < more
{
   RuntimeRequires(0 < y); // try changing this to 10 < y and see what happens
   more := x + y;
   less := x - y;
}

method RuntimeRequires(cond: bool)
   requires cond
{
  expect cond, "precondition failure";
}