2010 Formosan Summer School on Logic, Language, and Computation (FLOLAC '10)

en:seminar

Tyng-Ruey Chuang — 2010-07-09T10:44:25+08:00

The speakers and titles of the short talks in the seminar session (July 9 afternoon): * 2:00 pm - 2:50 pm * Kung Chen: Side-Effect Localization for Lazy, Purely Functional Languages via Aspects * Max Schaefer: Type Inference for Datalog with Complex Type Hierarchies

menu2

Tyng-Ruey Chuang — 2010-07-09T10:35:57+08:00

* 邏輯 * 函數編程 * 操作語意 * 指稱語意 * 程式建構與推理 * 使用 Frama-C * 研究討論

en:menu2

Tyng-Ruey Chuang — 2010-07-09T10:35:03+08:00

Courses * Logic * Functional Programming * Operational Semantics * Denotational Semantics * Program Construction and Reasoning * Using Frama-C * Seminar

logic

Max Schäfer — 2010-07-08T22:18:21+08:00

Lecturers: 謝邁思 Max Schäfer. This lecture aims to provide students with the logical background knowledge needed to understand and appreciate the other lectures. We will cover propositional and first-order classical logic, both from a semantic perspective and in the context of sequent calculus. Time permitting we will also take a brief look at logic programming in Datalog.

deno

Tyng-Ruey Chuang — 2010-07-08T15:14:14+08:00

Lecturers: 莊庭瑞 Tyng-Ruey Chuang. The purpose of this course is to equip students with some knowledge about basic domain theory, and about denotational semantics of functional programs and While programs. Course Materials * [Lecture notes (2010-07-08 updated)]. * [Slides (2010-07-08 updated)]. * [In-class exercise.] * [homework.] * [Another In-class exercise (new).]

en:frama-c

Pascal Cuoq — 2010-07-08T10:25:14+08:00

Lecturer: Pascal Cuoq. Frama-C is a framework for combining analysis techniques towards the analysis or verification of C code. Why C? C is widely use for embedded programming. In a tiny number of cases, the embedded software is critical: lives depend on it functioning as expected. These applications do, and will increasingly, take advantage of formal methods.

en:chap6_simple.c - created

Pascal Cuoq — 2010-07-08T08:13:11+08:00

/*@ requires n > 0; requires \valid(p+ (0..n−1)); assigns \nothing; ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i]; ensures \exists int e; 0 <= e <= n−1 && \result == p[e]; */ int max_seq(int* p, int n) { int res = p[0]; for(int i = 0; i < n; i++) { if (res < p[i]) { res = p[i]; } } return res; }

en:chap6_orig.c - created

Pascal Cuoq — 2010-07-08T08:11:58+08:00

/*@ requires n > 0; requires \valid(p+ (0..n−1)); assigns \nothing; ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i]; ensures \exists int e; 0 <= e <= n−1 && \result == p[e]; */ int max_seq(int* p, int n) { int res = *p; /*@ loop invariant 0 <= i <= n ; */ for(int i = 0; i < n; i++) { if (res < *p) { res = *p; } p++; } return res; }

en:solution_saturation.c - created

Pascal Cuoq — 2010-07-07T17:48:52+08:00

int min, max; /*@ requires min <= max ; assigns \nothing; ensures min <= \result <= max ; ensures (min <= x <= max) ==> (\result == x) ; */ int saturation(int x) { int res; if (x <= min) res = min; else if (x >= max) res = max; else res = x; return res; }

en:solution_array.c - created

Pascal Cuoq — 2010-07-07T17:47:47+08:00

int t[8]; /* Q0: Write the assigns clause in the contracts of functions init, incr, main. Q1: Verify the safety of function init. Q2: Verify the ACSL contract of function init. */ /*@ assigns t[0..7] ; ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ; */ void init(void) { int i; /*@ loop invariant \forall integer j ; (0 <= j < i) ==> (t[j] == 1) ; loop invariant 0 <= i <= 8 ; loop variant 8 - i ; */ for(i = 0; i < 8; i++) t[i] = 1; } /* Q3: Ver…

en:solution_compare.c - created

Pascal Cuoq — 2010-07-07T17:44:15+08:00

/*@ requires \valid_range(p,0,n-1); requires \valid_range(q,0,n-1); requires n >= 0 ; ensures (\forall integer i ; 0 <= i < n ==> p[i] == q[i]) ==> \result == 1; ensures !(\forall integer i ; (0 <= i < n) ==> (p[i] == q[i])) ==> \result == 0 ; */ int compare_arrays(int *p, int *q, int n) { int i; /*@ loop invariant 0 <= i <= n ; loop invariant \forall integer j; (0 <= j < i) ==> p[j] == q[j] ; …

en:compare.c - created

Pascal Cuoq — 2010-07-07T12:04:07+08:00

int compare_arrays(int *p, int *q, int n) { int i; for (i = 0; i < n; i++) if (p[n] != q[n]) return 0; return 1; }