From f0c044ebd634cfc48f8f0f4903fcafdec597e3bd Mon Sep 17 00:00:00 2001 From: tabarbe Date: Tue, 3 Aug 2010 23:57:53 +0000 Subject: Dafny: Port commit part 1/2: Committing changed files. Do not attempt to regenerate the Parser and Scanner files before the port of Boogie/Core is done, as these have undergone changes, but will not be committed until after the Core port. --- Source/Dafny/SccGraph.cs | 134 ++++++++++++++++++++++++++++++----------------- 1 file changed, 85 insertions(+), 49 deletions(-) (limited to 'Source/Dafny/SccGraph.cs') diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs index 0498f55d..c7be5420 100644 --- a/Source/Dafny/SccGraph.cs +++ b/Source/Dafny/SccGraph.cs @@ -1,4 +1,6 @@ +using System; using System.Collections.Generic; +using System.Diagnostics.Contracts; namespace Microsoft.Dafny { @@ -7,9 +9,18 @@ namespace Microsoft.Dafny { enum VisitedStatus { Unvisited, OnStack, Visited } class Vertex { public readonly Node N; - public readonly List! Successors = new List(); + public readonly List/*!*/ Successors = new List(); + public List SccMembers; // non-null only for the representative of the SCC + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(cce.NonNullElements(Successors)); + if(SccMembers!=null) + Contract.Invariant(cce.NonNullElements(SccMembers)); +} + public Vertex SccRepresentative; // null if not computed - public List SccMembers; // non-null only for the representative of the SCC + public int SccId; // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort // the following field is used during the computation of SCCs and of reachability public VisitedStatus Visited; @@ -22,18 +33,31 @@ namespace Microsoft.Dafny { public Vertex(Node n) { N = n; } - public void AddSuccessor(Vertex! v) { - Successors.Add(v); + public void AddSuccessor(Vertex v) { + Contract.Requires(v != null); + Successors.Add(v); } } - Dictionary! vertices = new Dictionary(); + + +[ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(vertices!=null); + Contract.Invariant(cce.NonNullElements(vertices.Values)); + if(topologicallySortedRepresentatives!=null) + Contract.Invariant(cce.NonNullElements(topologicallySortedRepresentatives)); + Contract.Invariant(!sccComputed || topologicallySortedRepresentatives != null); +} + + Dictionary/*!*/ vertices = new Dictionary(); bool sccComputed = false; - List topologicallySortedRepresentatives; // computed by the SCC computation - invariant sccComputed ==> topologicallySortedRepresentatives != null; + List topologicallySortedRepresentatives; // computed by the SCC computation + public int SccCount { get { ComputeSCCs(); - assert topologicallySortedRepresentatives != null; // follows from postcondition of ComputeSCCs and the object invariant + Contract.Assert( topologicallySortedRepresentatives != null); // follows from postcondition of ComputeSCCs and the object invariant return topologicallySortedRepresentatives.Count; } } @@ -53,15 +77,17 @@ namespace Microsoft.Dafny { /// /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it. /// - Vertex! GetVertex(Node n) { + Vertex GetVertex(Node n) { + Contract.Ensures(Contract.Result() != null); + Vertex v = FindVertex(n); if (v == null) { v = new Vertex(n); vertices.Add(n, v); if (sccComputed) { - assert topologicallySortedRepresentatives != null; // follows from object invariant + Contract.Assert( topologicallySortedRepresentatives != null); // follows from object invariant v.SccRepresentative = v; - v.SccMembers = new List(); + v.SccMembers = new List(); v.SccMembers.Add(v); v.SccId = topologicallySortedRepresentatives.Count; topologicallySortedRepresentatives.Add(v); @@ -76,7 +102,7 @@ namespace Microsoft.Dafny { Vertex FindVertex(Node n) { Vertex v; if (vertices.TryGetValue(n, out v)) { - assert v != null; // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!) + Contract.Assert( v != null); // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!) return v; } else { return null; @@ -110,19 +136,22 @@ namespace Microsoft.Dafny { return GetSCCRepr(n).SccId; } - Vertex! GetSCCRepr(Node n) { + Vertex GetSCCRepr(Node n) { + Contract.Ensures(Contract.Result() != null); + Vertex v = GetVertex(n); ComputeSCCs(); - assert v.SccRepresentative != null; // follows from what ComputeSCCs does + Contract.Assert( v.SccRepresentative != null); // follows from what ComputeSCCs does return v.SccRepresentative; } /// /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node. /// - public List! TopologicallySortedComponents() { + public List TopologicallySortedComponents() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); ComputeSCCs(); - assert topologicallySortedRepresentatives != null; // follows from object invariant + Contract.Assert( topologicallySortedRepresentatives != null); // follows from object invariant List nn = new List(); foreach (Vertex v in topologicallySortedRepresentatives) { nn.Add(v.N); @@ -134,11 +163,11 @@ namespace Microsoft.Dafny { /// Idempotently adds 'n' as a vertex and then returns the set of Node's in the strongly connected component /// that contains 'n'. /// - public List! GetSCC(Node n) { + public List GetSCC(Node n) {Contract.Ensures(cce.NonNullElements(Contract.Result>())); Vertex v = GetVertex(n); ComputeSCCs(); Vertex repr = v.SccRepresentative; - assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs + Contract.Assert( repr != null && repr.SccMembers != null); // follows from postcondition of ComputeSCCs List nn = new List(); foreach (Vertex w in repr.SccMembers) { nn.Add(w.N); @@ -150,13 +179,13 @@ namespace Microsoft.Dafny { /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component /// that contains 'n'. /// - public int GetSCCSize(Node n) - ensures 1 <= result; - { + public int GetSCCSize(Node n){ + Contract.Ensures( 1 <= Contract.Result()); + Vertex v = GetVertex(n); ComputeSCCs(); Vertex repr = v.SccRepresentative; - assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs + Contract.Assert( repr != null && repr.SccMembers != null); // follows from postcondition of ComputeSCCs return repr.SccMembers.Count; } @@ -168,24 +197,25 @@ namespace Microsoft.Dafny { /// of the vertices. /// void ComputeSCCs() - ensures sccComputed; { + Contract.Ensures( sccComputed); + if (sccComputed) { return; } // check if already computed // reset all SCC information - topologicallySortedRepresentatives = new List(); + topologicallySortedRepresentatives = new List(); foreach (Vertex v in vertices.Values) { v.Visited = VisitedStatus.Unvisited; v.SccMembers = null; } - Stack stack = new Stack(); + Stack stack = new Stack(); int cnt = 0; foreach (Vertex v in vertices.Values) { if (v.Visited == VisitedStatus.Unvisited) { SearchC(v, stack, ref cnt); } } - assert cnt == vertices.Count; // sanity check that everything has been visited + Contract.Assert( cnt == vertices.Count); // sanity check that everything has been visited sccComputed = true; } @@ -193,11 +223,13 @@ namespace Microsoft.Dafny { /// /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'. /// - void SearchC(Vertex! v, Stack! stack, ref int cnt) - requires v.Visited == VisitedStatus.Unvisited; - requires topologicallySortedRepresentatives != null; - ensures v.Visited != VisitedStatus.Unvisited; - { + void SearchC(Vertex/*!*/ v, Stack/*!*/ stack, ref int cnt){ + Contract.Requires(v != null); + Contract.Requires(cce.NonNullElements(stack)); + Contract.Requires( v.Visited == VisitedStatus.Unvisited); + Contract.Requires( topologicallySortedRepresentatives != null); + Contract.Ensures( v.Visited != VisitedStatus.Unvisited); + v.DfNumber = cnt; cnt++; v.LowLink = v.DfNumber; @@ -207,10 +239,10 @@ namespace Microsoft.Dafny { foreach (Vertex w in v.Successors) { if (w.Visited == VisitedStatus.Unvisited) { SearchC(w, stack, ref cnt); - v.LowLink = min{v.LowLink, w.LowLink}; + v.LowLink = Math.Min(v.LowLink, w.LowLink); } else if (w.Visited == VisitedStatus.OnStack) { - assert w.DfNumber < v.DfNumber || v.LowLink <= w.DfNumber; // the book also has the guard 'w.DfNumber < v.DfNumber', but that seems unnecessary to me, so this assert is checking my understanding - v.LowLink = min{v.LowLink, w.DfNumber}; + Contract.Assert( w.DfNumber < v.DfNumber || v.LowLink <= w.DfNumber); // the book also has the guard 'w.DfNumber < v.DfNumber', but that seems unnecessary to me, so this assert is checking my understanding + v.LowLink = Math.Min(v.LowLink, w.DfNumber); } } @@ -218,7 +250,7 @@ namespace Microsoft.Dafny { // The SCC containing 'v' has now been computed. v.SccId = topologicallySortedRepresentatives.Count; topologicallySortedRepresentatives.Add(v); - v.SccMembers = new List(); + v.SccMembers = new List(); while (true) { Vertex x = stack.Pop(); x.Visited = VisitedStatus.Visited; @@ -240,13 +272,13 @@ namespace Microsoft.Dafny { } foreach (Vertex v in vertices.Values) { - assert v.Visited != VisitedStatus.OnStack; + Contract.Assert( v.Visited != VisitedStatus.OnStack); if (v.Visited == VisitedStatus.Unvisited) { - List cycle = CycleSearch(v); + List cycle = CycleSearch(v); if (cycle != null) { List nodes = new List(); - foreach (Vertex v in cycle) { - nodes.Add(v.N); + foreach (Vertex v_ in cycle) { + nodes.Add(v_.N); } return nodes; // a cycle is found } @@ -263,12 +295,14 @@ namespace Microsoft.Dafny { /// w on the stack followed by the vertices (in reverse order) in the returned list, where /// w is the first vertex in the list returned. /// - List CycleSearch(Vertex! v) - requires v.Visited == VisitedStatus.Unvisited; - ensures v.Visited != VisitedStatus.Unvisited; - ensures result == null ==> v.Visited == VisitedStatus.Visited; - ensures result != null ==> result.Count != 0; + List CycleSearch(Vertex v) { + Contract.Requires(v != null); + Contract.Requires( v.Visited == VisitedStatus.Unvisited); + Contract.Ensures( v.Visited != VisitedStatus.Unvisited); + Contract.Ensures( Contract.Result>() != null || v.Visited == VisitedStatus.Visited); + Contract.Ensures( Contract.Result>() == null || Contract.Result>().Count != 0); + v.Visited = VisitedStatus.OnStack; foreach (Vertex succ in v.Successors) { // todo: I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking. @@ -276,7 +310,7 @@ namespace Microsoft.Dafny { // there is no cycle in the subtree rooted at succ, hence this path does not give rise to any cycles } else if (succ.Visited == VisitedStatus.OnStack) { // we found a cycle! - List cycle = new List(); + List cycle = new List(); cycle.Add(succ); if (v == succ) { // entire cycle has been found @@ -284,8 +318,8 @@ namespace Microsoft.Dafny { } return cycle; } else { - assert succ.Visited == VisitedStatus.Unvisited; - List cycle = CycleSearch(succ); + Contract.Assert( succ.Visited == VisitedStatus.Unvisited); + List cycle = CycleSearch(succ); if (cycle != null) { if (succ.Visited == VisitedStatus.Visited) { // the entire cycle has been collected @@ -321,7 +355,9 @@ namespace Microsoft.Dafny { return ReachSearch(a, b); } - bool ReachSearch(Vertex! source, Vertex! sink) { + bool ReachSearch(Vertex source, Vertex sink) { + Contract.Requires(source != null); + Contract.Requires(sink != null); if (source == sink) { return true; } else if (source.Gen == generation) { @@ -329,7 +365,7 @@ namespace Microsoft.Dafny { return false; } else { source.Gen = generation; - return exists{Vertex succ in source.Successors; ReachSearch(succ, sink)}; + return Contract.Exists(source.Successors,succ=> ReachSearch(succ, sink)); } } } -- cgit v1.2.3