From 2541e9de002267359897bf967755172fcc726512 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 22 Oct 2012 02:18:51 -0700 Subject: renamed "abstract module" to "module facade" renamed "ghost module" to "abstract module", adding a keyword "abstract" --- Test/dafny1/SchorrWaite-stages.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/dafny1') diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 094e7be7..63c55506 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -4,7 +4,7 @@ // Version with proof divided into stages: June 2012. // Copyright (c) 2008-2012 Microsoft. -ghost module M0 { +abstract module M0 { // In this module, we declare the Node class, the definition of Reachability, and the specification // and implementation of the Schorr-Waite algorithm. @@ -140,7 +140,7 @@ ghost module M0 { } } -ghost module M1 refines M0 { +abstract module M1 refines M0 { // In this superposition, we start reasoning about the marks. In particular, we prove that the method // marks all reachable nodes. method SchorrWaite... @@ -176,7 +176,7 @@ ghost module M1 refines M0 { } } -ghost module M2 refines M1 { +abstract module M2 refines M1 { // In this superposition, we prove that only reachable nodes are marked. Essentially, we want // to add a loop invariant that says t is reachable from root, because then the loop invariant // that marked nodes are reachable follows. More precisely, we need to say that the node -- cgit v1.2.3