Conversation
|
|
||
| } | ||
|
|
||
| fn skjkasdkd(lst: Vec<u32>) -> (ret: u32) |
There was a problem hiding this comment.
This is a really weird keyboard-mash of a function name. I realize it's the one the prompt chose, but I think it would help to add a comment to that effect, so future readers aren't puzzled by it.
tasks/human_eval_094.rs
Outdated
| spec_find_largest_prime( | ||
| lst@.map_values(|val: u32| val as nat) | ||
| ) as nat | ||
| ) || ret == 0 |
There was a problem hiding this comment.
The English spec doesn't say what to do if the input doesn't have any prime values. I would lean towards adding a precondition that the list does indeed contain at least one prime value. That way you can remove the || ret == 0. If you want to avoid a precondition, then I think the idiomatic approach would be to return Option<u32>, and then to specify in the postcondition that None implies there were no prime values in the input. If you don't include that condition, then a trivial implementation can satisfy the spec by always returning None (or 0 with the current spec).
There was a problem hiding this comment.
Looking at the canonical it seems to me the default behavior is returning 0 if no primes are found:
def skjkasdkd(lst):
def isPrime(n):
for i in range(2,int(n**0.5)+1):
if n%i==0:
return False
return True
maxx = 0
i = 0
while i < len(lst):
if(lst[i] > maxx and isPrime(lst[i])):
maxx = lst[i]
i+=1
result = sum(int(digit) for digit in str(maxx))
return result
but it is also true that spec_find_largest_prime will return 0 if it takes a list without a prime anyways, so it seems the || ret == 0 clause is redundant in the specification anyways.
tasks/human_eval_094.rs
Outdated
| if i <= 0 { | ||
| 0 | ||
| } else { | ||
| let first_i = s.take(i as int); // first i digits |
There was a problem hiding this comment.
Here and in the rest of the comments, I think you want "integers"/"numbers", not "digits"
2 participants
94 was completed with advice from @elanortang, and 97 was a joint effort between @SSSPigeon and I.
Used Verus version 2025.08.23.bb6fd4e pinned here.