From 8c9eb700f6eb6c3c3da4f6882ea8f29aa10eb06a Mon Sep 17 00:00:00 2001 From: MRHMisu Date: Fri, 27 Sep 2024 11:37:59 -0700 Subject: [PATCH] Update parameter types and add comments --- tasks/human_eval_082.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_082.rs b/tasks/human_eval_082.rs index ffa408f..4afb97a 100644 --- a/tasks/human_eval_082.rs +++ b/tasks/human_eval_082.rs @@ -9,11 +9,13 @@ use vstd::prelude::*; verus! { -spec fn is_divisible(n: int, divisor: int) -> bool { +pub open spec fn is_divisible(n: int, divisor: int) -> bool { (n % divisor) == 0 } -fn prime_length(str: &Vec) -> (result: bool) +// Implementation following the ground-truth +// This function determines if a given string length is prime or not +fn prime_length(str: &[char]) -> (result: bool) ensures result == if str.len() < 2 { false