MAP/i - Foundations of Computing

Assessment

Part I

Write and present a short report in one of the topics.

Bibliography.

Formulae-as-types as a notion of control

Groups:

1. Bruno Oliveira and Vitor Rodrigues: Theme 5

2. Alexandre Madeira and Miguel Ferreira: Theme 1

3. Hugo Pacheco and Miguel Marques: Theme 2

4. Luis Santos and Ricardo Freitas: Theme 6

5. Hugo Conceição: Theme 3

6. José Pedro Oliveira: Theme 4

Part II

Coq mini-projects:

Binary Integers

The aim of this mini-project is to enconde binary integers as lists of booleans. That is:

Require Import ZArith.
Require Import List.
Require Import Bool.
Open Scope Z_scope.

Definition BInt := list bool.

Fixpoint toZ (x : BInt) : Z :=
 match x with
 | nil => 0
 | true :: xs => 1 + 2*(toZ xs)
 | false :: xs => 2*(toZ xs)
 end.

(observe that the head of the list is the least significant bit)

1. - Define the following functions:
   • bSucc - computes the successor of a binary integer
   • bAdd - computes the addition of two binary integers
   • bMult - computes multiplication of two binary integers
2. - Prove the correctness of those functions (e.g. forall x, toZ (bSucc x)=1+(toZ x))

NOTE: in the definition of bAdd, it is convenient to simultaneously define a function bAddCarry (performs addition with carry). Use the "Fixpoint ... with ..." to accomplish these simultaneous definitions.

Declarative Arrays

A possible encoding of arrays in Coq is through axiomatization of the corresponding theory. E.g. (taken from the Why tool)

(* The type of arrays *)
Parameter raw_array : Set -> Set.
Definition array (T:Set) := prod Z (raw_array T).

(* Array length *)
Definition array_length (T:Set) (t:array T) : Z := let (n, _) := t in n.

(* Functions to create, access and modify arrays *)
Parameter raw_new : forall T:Set, T -> raw_array T.
Definition new (T:Set) (n:Z) (a:T) : array T := (n, raw_new a).
Parameter raw_access : forall T:Set, raw_array T -> Z -> T.
Definition access (T:Set) (t:array T) (i:Z) : T :=
  let (_, r) := t in raw_access r i.
Parameter
  raw_update : forall T:Set, raw_array T -> Z -> T -> raw_array T.
Definition update (T:Set) (t:array T) (i:Z) (v:T) : array T :=
  (array_length t, let (_, r) := t in raw_update r i v).

(* Update does not change length *)
Lemma array_length_update :
 forall (T:Set) (t:array T) (i:Z) (v:T),
   array_length (update t i v) = array_length t.
Proof.
trivial.
Qed.

(* Axioms *)
Axiom
  new_def :
    forall (T:Set) (n:Z) (v0:T) (i:Z),
      (0 <= i < n)%Z -> access (new n v0) i = v0.

Axiom
  update_def_1 :
    forall (T:Set) (t:array T) (v:T) (i:Z),
      (0 <= i < array_length t)%Z -> access (update t i v) i = v.

Axiom
  update_def_2 :
    forall (T:Set) (t:array T) (v:T) (i j:Z),
      (0 <= i < array_length t)%Z ->
      (0 <= j < array_length t)%Z ->
      i <> j -> access (update t i v) j = access t j.

1. - Define a function sumArray to compute the sum of elements in an array.
2. - Formulate and prove the correctness of the previously defined function.

Paper Reading

• A Tutorial on Recursive Types in Coq. Eduardo Gimenez and Pierre Casteran. link

• Efficient Weakest Preconditions. K. Rustan M. Leino. link

• Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Mike Barnett, Bor-Yuh Evan Chang, Robert deLine, Bart Jacobs, and K. Rustan M. Leino. link

• A Certifying Compiler for Java. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, Kenneth Cline. link

• Foundational Proof-Carrying Code. Andrew W. Appel. link

• Proof Obligations Preserving Compilation (Extended abstract). Gilles Barthe, Tamara Rezk and Ando Saabas. link

• Universes: Lightweight Ownership for JML. Werner Dietl and Peter Mueller. link

• Beyond Assertions: Advanced Specification and Verification with JML and ESC / Java2. Patrice Chalin, Joseph Kiniry, Gary T. Leavens and Erki Poll. link

Part III

Workshop "Program Semantics, Verification, and Construction" 16/02/2008

10h-11h45 Part 1:

1. Alexandre Madeira, Miguel Ferreira. "Combinatory logic"

2. Hugo Pacheco. "Expressibility: the simply typed lambda-calculus (vs. the pure system), system T"

3. Bruno Oliveira, Vitor Rodrigues. "Type systems I"

4. Luis Santos, Ricardo Freitas. "Type system II"

Part 2: 12h-13h45

1. Bruno Oliveira. "Efficient Weakest Preconditions"

2. Vitor Rodrigues, Ricado Freitas. "Beyond assertions: Advanced specification and verification with JML and ESC/Java2"

3. Alexandre Madeira. "Pointfree Factorization of Operation Refinement"

4. Hugo Pacheco. "Tupling calculation eliminates multiple data traversal"