1

It seems intuitively clear that the effect of the following two methods are identical, if one ignores intermediate stages:

method print1()
{
    print "hello, world\n";
}

method print2()
{
    print "hello, ";
    print "world";
    print "\n";
}

Is there a way to assert the equivalence of side effects for these two methods?

akiarie
  • 49
  • 4

1 Answers1

4

No, there's no builtin way to do this.

Even if there was, it wouldn't support the many operations not built in to Dafny that are needed to connect a program to the real world, such as reading input.

If you want to do something like that, the way to do it is to build a logical model of the aspects of the side effect that you care about capturing, and then axiomatize the fact that the primitive operations satisfy their specifications.

(You might find this unrelated answer about file IO useful as a starting point, but it does not address the question of logical modeling.)

James Wilcox
  • 5,307
  • 16
  • 25
  • Are you aware of any verification systems that support this, say Frama C? – akiarie Jun 28 '23 at 05:18
  • 1
    No, and in fact, in the most common logical model I am aware of (tracking the sequence of system calls made), these two programs are not equivalent, because they make different sequences of system calls. – James Wilcox Jul 03 '23 at 20:31