hwayne

------------------------------ MODULE server_2 ------------------------------
EXTENDS TLC, Integers, Sequences
CONSTANTS MaxQueueSize

(*--algorithm message_queue

variable queue = <<>>;

define
  BoundedQueue == Len(queue) <= MaxQueueSize 

hwayne

from dpcontracts import require, ensure
# https://github.com/deadpixi/contracts
# with a regular postcondition

@ensure("List is sorted", lambda a, r: all((x <= y for (x, y) in zip(r, r[1:]))))
def bubble_sort(arr):
    n = len(arr)
    new_arr = arr[:]
    for i in range(n):
        for j in range(0, n-i-1):

hwayne

method Unique(a: seq<int>) returns (b: seq<int>)
  ensures forall k :: 0 <= k < |a| ==> a[k] in b
  ensures forall i, j :: 0 <= i < j < |b| ==> b[i] != b[j]
{
  var index := 0;
  b := [];
  while index < |a|
    invariant index <= |a|
    invariant forall i, j :: 0 <= i < j < |b| ==> b[i] != b[j]
    invariant forall k :: 0 <= k < index ==> a[k] in b

hwayne

Snapshot
  logout -> Login Page
  Reports
    summary -> Summary
    students -> Students
    standards -> Standards
    Summary*
    Students
      answer -> Answers
    Standards

hwayne

Snapshot
  logout -> Login Page
  Reports
    summary -> Summary
    students -> Students
    standards -> Standards
    Summary*
    Students
      answer -> Answers
    Standards

hwayne

datatype Option<T> = None | Some(x: T)

method BinarySearch(haystack: array<int>, needle: int) returns (n: Option<int>) 


requires forall i, j :: 0 <= i <= j < haystack.Length ==> haystack[i] <= haystack[j]
ensures n.Some? ==> 
    0 <= n.x < haystack.Length && haystack[n.x] == needle
ensures n.None? ==> 
    forall i :: 0 <= i < haystack.Length ==> haystack[i] != needle

hwayne

//This is the one that Daniel Jackson wrote

 abstract sig Node {inputs: set Node}

 sig Source extends Node {} {no inputs}
 sig Sink extends Node {} {one inputs}

 abstract sig Gate extends Node {}
 sig And, Or, Xor extends Gate {} {#inputs = 2}
 sig Not extends Gate {}  {one inputs}

hwayne

const int total_dropped;

S =? [ dropped = total_dropped]

P =? [ (F queue = MAX) & (F "done" & dropped = total_dropped)]

hwayne

Constraints:

• At most one of sulfuras?, pass?, and brie? are true

Assuming whenever they say "increases or decreases" without a qualifier, they mean 1. This is a BIG assumption (it's not specified).

sulfuras?	pass?	brie?	days_left	change
T	-	-	-	0
F	T	-	11-	+1

hwayne

proc write(key: str, value: T) modifies store {
  store[key] := value;
}

fun read(key: str) returns (out:T)  {
  out := store[key];
}

// ....