You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
txiang61 opened this issue
Sep 6, 2024
· 2 comments
Labels
incompletenessThings that Dafny should be able to prove, but can'tkind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lemma Proof<A>(x: seq<A>, b: A) {
if |x| == 1 {
assert x == [x[0]];
var p := a => [b];
// assert p(x[0]) == [b]; // useless// var _ := Concat(Map(x, p)); // uselessassertMap(x, p) == [[b]]; // This line and the next are both neccessaryassertConcat([[b]]) == [b];
// The following assertions can replace the two previous assertions// assert Foo(x, p) == Concat(Map(x, p));assertFoo(x, p) == [b];
}
}
function Foo<A>(actions: seq<A>, b: A ->seq<A>): seq<A> {
Concat(
Map(
actions,
b
))
}
function Map<T, U>(s: seq<T>, f: T -> U): (res: seq<U>) {
if s == [] then []
else [f(s[0])] +Map(s[1..], f)
}
function Concat<A>(s: seq<seq<A>>): (res: seq<A>) {
if s == [] then []
else s[0] +Concat(s[1..])
}
Command to run and resulting output
No response
What happened?
Sometimes copying over the function body can prove the assertions. The example above is a short and simple but in practice the function aren't as small as the one above. The real pain comes from having to copy over the whole function body in order to prove some assertions.
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered:
txiang61
added
the
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
label
Sep 6, 2024
incompletenessThings that Dafny should be able to prove, but can'tkind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Dafny version
4.4.0
Code to produce this issue
Command to run and resulting output
No response
What happened?
Sometimes copying over the function body can prove the assertions. The example above is a short and simple but in practice the function aren't as small as the one above. The real pain comes from having to copy over the whole function body in order to prove some assertions.
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: