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

Initial commit.

parents
No related branches found
No related tags found
No related merge requests found
{
"folders": [
{
"path": "demonstration"
},
{
"path": "practice"
}
],
"settings": {
"files.eol": "LF",
"files.trimFinalNewlines": true,
"files.trimTrailingWhitespace": true
}
}
\ No newline at end of file
method minimum_of_three(first: real, second: real, third: real) returns (minimum: real)
ensures minimum in {first, second, third}
ensures minimum <= first
ensures minimum <= second
ensures minimum <= third
{
var result := first;
if second < first && second < third {
result := second;
}
if third < first && third < second {
result := third;
}
return result;
}
method count_leading_zeros(sequence: seq<nat>) returns (count: nat)
ensures count <= |sequence|
ensures
forall i | 0 <= i < count ::
sequence[i] == 0
ensures count < |sequence| ==> sequence[count] != 0
{
var index := 0;
while index < |sequence| {
if sequence[index] != 0 {
break;
}
index := index + 1;
}
return index;
}
method list_to_set<T>(list: seq<T>) returns (as_set: set<T>)
requires
forall i | 0 <= i < |list| ::
forall j | i < j < |list| ::
list[i] != list[j]
ensures |as_set| == |list|
{
var result := {};
var index := 0;
while index < |list| {
result := result + {list[index]};
index := index + 1;
}
return result;
}
method set_to_list<T>(collection: set<T>) returns (as_list: seq<T>)
ensures |as_list| == |collection|
ensures
forall x | x in collection ::
x in as_list
{
var result := [];
var remaining := collection;
while |remaining| > 0 {
var element :| element in remaining;
remaining := remaining - {element};
result := result + [element];
}
return result;
}
method copy_values<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updated_mapping: map<T, U>)
requires
forall k | k in mapping && k in sources ::
sources[k] in mapping
{
var result := map[];
var remaining := set key | key in mapping :: key;
while |remaining| > 0 {
var destination_key :| destination_key in remaining;
remaining := remaining - {destination_key};
var source_key := destination_key;
if destination_key in sources {
source_key := sources[destination_key];
}
result := result[destination_key := mapping[source_key]];
}
return result;
}
method map_f<T, U>(f: T -> U, inputs: seq<T>) returns (outputs: seq<U>)
ensures |outputs| == |inputs|
ensures
forall i | 0 <= i < |outputs| ::
outputs[i] == f(inputs[i])
{
var results := [];
var index := 0;
while index < |inputs| {
results := results + [f(inputs[index])];
index := index + 1;
}
return results;
}
method reverse<T>(list: seq<T>) returns (reversed: seq<T>)
ensures |reversed| == |list|
ensures
forall i | 0 <= i < |reversed| ::
reversed[i] == list[|list| - i - 1]
{
var result := [];
var index := |list|;
while index > 0 {
index := index - 1;
result := result + [list[index]];
}
return result;
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment