SENG2011 Complete comprehensive notes including workings PDF

Preview

Summary

Includes workings - extremely comprehensive. Good luck for the exams! Hopefully you are all going to smash it....

Description

lukakerr.github.io

About

Projects

Uni

Code

Misc

RSS Feed

Written by Luka Kerr on November 23, 2019

Dafny Dafny is a Microsoft research project that acts as a static verifier. It translates to Boogie, the backend, which interacts with Z3, a SMT solver. method Main() { assert 1 == 1; print "hello, world\n"; }

Correctness Dafny can prove your code is correct, meaning it can: Guarantee array indices stay in bounds Guarantee no null dereferences Guarantee no division by zero Guarantee the program conforms to a specification

Types Dafny has various inbuild types: bool for booleans char for characters real , int , nat for real, unbounded and natural numbers set , seq for immutable finite sets and sequences array for arrays array2 for 2D arrays object is a super-type of all reference types

Methods Methods in Dafny are like functions or procedures in conventional languages. Input parameters and output arguments are typed as follows: method Add(x: int, y: int) returns (sum: int) { sum := x + y; }

}

Input parameters are immutable. A return statement is not necessary in a method, but if there is one, it need not have arguments or it must have all the return arguments of the method.

Functions Functions in Dafny are only used in verification. They are side effect free and consist of a single expression that yields a value of some type. function One(): int { 1 }

Function Methods Function methods combine functions and methods, allowing functions to be used in verification and implementation. function method One(): int { 1 }

Predicates A predicate is used for verification only. It is a special type of function in that it returns a bool only.

predicate Sorted(a: array) reads a { forall j, k :: 0 a[j] for boolean operations

Operations Dafny has various built in operations, including: assert that evaluates a boolean expression during verification requires that declares a pre-condition by evaluating a boolean expression during

verification ensures that declares a post-condition by evaluating a boolean expression during

verification method Square(x: int) returns (y: int) requires x >= 0 ensures y == x*x { y := x*x; assert y > x; }

Arrays In Dafny, arrays are mutable data structures and are stored on the heap. The length of an array a can be accessed with a.Length , and array indexes range from 0 to a.Length - 1 .

Arrays are created with the new keyword: var a: array := new char[5]; . modifies

To minimise the verifier’s work, a modifies keyword can be used to tell the verifier that an array will be modified. reads

If a function has an array input argument, then a reads statement is required.

Sets A set set is an orderless collection of elements that is immutable. There are various operations that can be performed on sets var s1: set := {4, 5, 6}; var s2: set := {1, 2, 3};

s1 != s2 s1 == s2 s1 + s2

// not equal to comparison // equal to comparison // set union

s1 * s2 s1 - s2 s1 forall k :: 0 a[k] != key { i := 0; while i < a.Length invariant 0...