Add files via upload

factorial.dfy

@@ -0,0 +1,20 @@
+function fact (n:nat) : nat
+decreases n
+{
+    if n <= 0 then 1 else n*fact(n-1)
+}
+method Factorial(n: nat) returns (p: nat)
+requires n>=0
+ensures p == fact(n)
+{
+    var i : nat;
+    i, p := 1,1;
+    while i <= n
+    invariant i<= n+1
+    invariant p == fact(i-1)
+    decreases n + 1 - i
+    {
+        p := p * i;
+        i := i + 1;
+    }
+}

fibonacci.dfy

@@ -0,0 +1,23 @@
+function fib(n: nat): nat
+decreases n
+{
+    if n<=1 then n else fib(n-1)+fib(n-2)
+}
+method fibfast(n: nat) returns (c: nat)
+requires n>=1;
+ensures c==fib(n);
+{
+    var p := 0;
+    c := 1;
+    var i := 1;
+    while(i<n)
+    invariant 1<=i<=n
+    invariant p == fib(i-1) && c == fib(i)
+    decreases (n-i)
+    {
+        var new2 := p + c;
+        p := c;
+        c := new2;
+        i := i + 1;
+    }
+}

firstRefresh.dfy

@@ -0,0 +1,36 @@
+method Swap(a: int, b: int) returns (x: int, y: int)
+ensures x == b && y == a;
+{
+    x := b;
+    y := a;
+}
+method Warn()
+{
+    var x;
+    x := 1;
+    assert x < 10;
+    assert x < 100;
+}
+function fact(n : nat): nat
+decreases n
+{
+    if n == 0 then 1 else n*fact(n-1)
+}
+method Factorial (n: nat) returns (p: nat)
+requires n >= 0;
+{
+    var i: int;
+    i, p := 1, 1;
+    while (i <= n)
+    invariant i <= n + 1;
+    invariant p <= p * i;
+    decreases n + 1 - i;
+    {
+        p := p * i;
+        i := i + 1;
+    }
+}
+method something(){
+    var f : int; 
+    f := Factorial(0);
+}

inversemod.dfy

@@ -0,0 +1,98 @@
+method inversemod(a: nat, n: nat) returns (t: nat, flag: bool)
+requires a>0 && n>0;
+ensures (!flag ==> t == 1) || (flag ==> (a*t)%n==1)
+{
+    var x := 0;
+    while x<=a && (1+n*x)%a!=0
+    invariant 0<=x<=a+1
+    decreases (a-x) {
+        x := x + 1;
+    }
+    if (x == a+1){
+        flag := false; t := 1;
+    }
+    else{
+        flag := true; t := (1+n*x)/a;
+    }
+}
+function power(b: nat, e: nat): nat 
+decreases e
+{
+    if e == 0 then 1 else b * power(b,e-1)
+}
+method expoBySquare(x:nat,n:nat) returns (p:nat)
+requires n>=0
+ensures p == power(x,n)
+decreases *
+{
+    var N,q := n,x;
+    p := 1;
+    while N>=0
+    decreases *
+    {
+        p := if N%2 == 0 then p else p*q;
+        q := q * q;
+        N := if N%2 == 0 then N/2 else (N-1)/2;
+    }
+}
+function fact (n:nat) : nat
+requires n >= 0
+decreases n
+{
+    if n <= 0 then 1 else n*fact(n-1)
+}
+method Factorial(n: nat) returns (p: nat)
+requires n>=0
+ensures p == fact(n)
+{
+    var i : nat;
+    i, p := 1,1;
+    while i <= n
+    invariant i<= n+1
+    invariant p == fact(i-1)
+    decreases n + 1 - i
+    {
+        p := p * i;
+        i := i + 1;
+    }
+}
+class primeRandomNumber{
+    var xk: nat;
+    constructor()
+    ensures xk == 4;
+    {
+        xk := 4;
+    }
+    method primePRNG() returns (r: nat)
+    modifies this
+    ensures xk == (12*old(xk))%40
+    ensures 40 < r < 1602
+    {
+        xk := (12*xk)%40;
+        r  := xk*xk + xk + 41;
+    }
+}
+method RSAencrypt (m: nat) returns (c: nat, flag: bool)
+requires m>=0
+decreases *
+{
+    var m1: nat; var f2: bool;
+    var h := new primeRandomNumber();
+    var p := h.primePRNG();
+    var q := h.primePRNG();
+    var n := p * q;
+    var ph :=(p-1)*(q-1);
+    var e := h.primePRNG();
+    var d, f1 := inversemod(e,ph);
+    if (f1){
+        c := expoBySquare(m,e);
+        c := c % n;
+        m1 := expoBySquare(c,d);
+        m1 := m1 % n;
+        f2 := (m==m1);
+        flag := f2 && f1;
+    }else{
+        flag := true;
+        c := 9999;
+    }
+}

pell.dfy

@@ -0,0 +1,23 @@
+method pellEquations (n: int) returns (flag: bool,x: int, y: int)
+requires 0<=n
+// ensures flag ==> x*x-n*y*y == 1
+// ensures !(flag) ==> (x==99 && y==99)
+{
+    var m3: int;
+    m3 := 0;
+    flag := false;
+    while m3 <= 100*100 - 1
+    invariant m3 <= 100*100
+    invariant ((m3/100)*(m3/100)-n*(m3%100)*(m3%100))!=1
+    decreases 100*100 - m3
+    {
+        x := m3/100;
+        y := m3%100;
+        if (x*x-n*y*y)!=1
+        {
+            flag := true;
+            break;
+        }
+        m3 := m3 + 1;
+    }
+}

powerExp.dfy

@@ -0,0 +1,20 @@
+function power(b: nat, e: nat): nat 
+decreases e
+{
+    if e == 0 then 1 else b * power(b,e-1)
+}
+method expoBySquare(x:nat,n:nat) returns (p:nat)
+requires n>=0
+ensures p == power(x,n)
+decreases *
+{
+    var N,q := n,x;
+    p := 1;
+    while N>=0
+    decreases *
+    {
+        p := if N%2 == 0 then p else p*q;
+        q := q * q;
+        N := if N%2 == 0 then N/2 else (N-1)/2;
+    }
+}