Hi,
There's an inconsistency I think with the ground-truth specification in human_eval/problem_2. It currently states the following
def problem_spec
-- function signature
(impl: Rat → Rat)
-- inputs
(number: Rat) :=
-- spec
let spec (res) :=
0 ≤ res ∧
res < 1 ∧
number.floor + res = number;
number > 0 →
-- program terminates
(∃ result, impl number = result ∧
-- return value satisfies spec
spec result)
The program termination and result property satisfaction are here expressed as consequence of the precondition. This is the only instance of this kind I could find: in all other entries the precondition is expressed inside the spec definition, and is thus semantically different.
I believe this is an one-off anomaly, as I could not think of a reason why this problem would require a different handling (termination conditional on the precondition being met). If you agree, I will submit a PR addressing this.
Hi,
There's an inconsistency I think with the ground-truth specification in human_eval/problem_2. It currently states the following
The program termination and result property satisfaction are here expressed as consequence of the precondition. This is the only instance of this kind I could find: in all other entries the precondition is expressed inside the
specdefinition, and is thus semantically different.I believe this is an one-off anomaly, as I could not think of a reason why this problem would require a different handling (termination conditional on the precondition being met). If you agree, I will submit a PR addressing this.