MAP/i - Foundations of Computing

Option I: Program Semantics, Verification, and Construction

Part I

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


Formulae-as-types as a notion of control


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)
(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.
  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.

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

  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.

  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"

  Attachment Action Size Date Who Comment
pdf props, move 250.5 K 10 Nov 2008 - 23:19 NelmaMoreira? A Formulae-as-types notion of control
r14 - 07 Dec 2010 - 22:42:59 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM