Skip to content
Snippets Groups Projects
Commit bed1f2d0 authored by Brady James Garvin's avatar Brady James Garvin
Browse files

Made various typo fixes and clarifications.

parent cf9192a4
Branches master
No related tags found
No related merge requests found
......@@ -48,11 +48,11 @@ predicate isValidGraph<T>(graph: map<T, set<T>>) {
// Because of the representation chosen, iterating over the neighbors of a vertex means iterating over a set, which is tricky in Dafny. For reference, such a
// loop should look like:
// var neighbors := graph[vertex];
// var neighbors := graph[vertex]; // track the neighbors that we still need to loop over
// while |neighbors| > 0 {
// var neighbor :| neighbor in neighbors; // this line means "choose any one neighbor from the neighbors set"
// neighbors := neighbors - {neighbor};
// // [so something with neighbor]
// var neighbor :| neighbor in neighbors; // choose any one neighbor from the neighbors set
// neighbors := neighbors - {neighbor}; // remove that neighbor from the set
// // [do something with the neighbor]
// }
// We represent a path in a graph as a nonempty sequence of vertices. Again, not all sequences are valid paths. For example, in the graph {A: {B}, B: {}}, the
......@@ -79,11 +79,11 @@ predicate hasAllEdgeSourcesIn<T>(path: seq<T>, vertices: set<T>) {
forall i | 0 <= i < |path| - 1 :: path[i] in vertices
}
// And given a collection of such paths, it is useful to be able to ask what those final vertices are:;
// And given a collection of such paths, it is useful to be able to ask what those final vertices are:
function finalVertices<T>(paths: seq<seq<T>>) : set<T>
requires forall i | 0 <= i < |paths| :: |paths[i]| > 0
{
(set i | 0 <= i < |paths| :: paths[i][|paths[i]|-1])
set i | 0 <= i < |paths| :: paths[i][|paths[i]|-1]
}
// Finally, we provide two lemmas to summarize facts that are obvious to humans but not so obvious to Dafny.
......@@ -137,7 +137,7 @@ method search<T>(graph: map<T, set<T>>, begin: T, end: T) returns (path: seq<T>)
while |worklist| > 0
decreases vertices - visited, worklist
{
var workitem;
var workitem: seq<T>;
worklist, workitem := pop(worklist);
var final := workitem[|workitem|-1];
if final == end {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment