| Week 1 | | | Week 5 | | | Week 9 | |
| Week 2 | | | Week 6 | | | Week 10 | |
| Week 3 | | | Week 7 | | | Week 11 | |
| Week 4 | | | Week 8 | | | Week 12 |
Our first lecture.
Martí Grau:The lecture began with an introduction by Joost on the aim of the company and the reverse engineering nature of software verification. It was briefly mentioned that the process involves finding a proof in intuitionistic logic, which will correspond to a program. Then Ana spoke about getting witnesses in intuitionistic proofs, and how some equivalences in classical logic don't hold in intuitionistic logic, such as ∃ α ≢ ¬ ∀ ¬ α. The course will first deal with inductive definitions and recursion. Thus, we began trying to come up with some examples of inductive definitions, namely for the natural numbers (or "aliens"), their addition, their product, their factorial function and the function of "being less than".
Having given examples of inductive definitions and recursive functions in the last class, this week we have re-written them in OCaml language. We have started to learn the basics of OCaml programming, its syntax and how to define types and recursive functions and its difference with other programming languages. We have written in OCaml the type "natural number" (or aliens) and "list" (or queue) and the recursive functions of the sum and product of natural numbers, the length and total of a list (that returns the number of elements of a list and its sum, respectively) and the functions below_n, map and <t.
Martí Arnau:
In the last class, which was led by Joost, we briefly reviewed the goals recently set in the quarterly business meeting: 1) to come up with both a Driver's List and an Activity List from the Tachograph's data and 2) to develop an Events List and a list of Finable Objects.
Then we touched upon the notion of types and their ability to specify the kinds of entities we work with. We saw that type checking, i.e. the automatic procedure through which OCaml infers the type of a certain term, is done by means of a derivation. For example, we wrote the derivation needed to establish that A(O, A(O, E) is of type queue.Finally, we corrected a coupe of exercises that we had trouble with: [elim] and [range]. We recursively defined and used an abbreviation of queue to write queues more easily in the following way:
[ ] := E
[a, x0, ... , xn] := A(a, [x0, ... , xn])
When solving [range] we realized that, if carefully read, the statement has some ambiguities (Joost pointed out that this process of finding ambiguities and deciding how to interpret them is very common when formalizing the law):
The solution we devised for [range] (and was or wasn't it the one Ana had thought of?) was the following:
let rec range l r =
match r with
I O -> if eq l O
then [O]
else E
I Sd -> if lt Sd l
then E
else if eq l Sd
then Sd
else [range l d, Sd];;
Alba Porras: The 5/4/18 class we saw the main types of Ocaml programming language and also its basic syntax. Ana taught us to implement basic functions such as addition. We also talk about the syntax of lists and polymorphic variables. Finally we saw lists in which the type of variable of its elements is not specified.
Gina Tarrach: In today's class we have talked about different aspects of OCaml's programming language. Firstly, we have learned how to specify the type of the inputs and the output of a function, instead of letting OCaml figure it out. We have then talked about local and global identifiers, its differences and when and how to use local ones. Lastly, we have introduced (and put into practice) another type of recursion: tail recursion, which is more efficient and less memory and time consuming than the "standard" one.
Alba Porras: The class began with a review of propositional logic. We saw an inductive definition of the formulas.
Then we started to learn how to encode the propositional logic in Ocaml:
First, we defined the type 'variable'.
Second, we defined the type 'formula' like this:
type formula =
(*basic cases: *)
|var of variable (*an object of type variable*)
|Bot (*falsum*)
(*inductive cases: *)
|Neg of formula (*for the negation *)
|And of formula * formula (* for the conjunction*);;
Thus, a phi formula can give us an output such as: And (Bot, Neg Bot);;
As this way of defining the formulas can be difficult to read, we defined the functions string_of_variable and string_of_formula to use symbols more similar to those of the propositional logic.
Finally, we define the function is_tauto that given a formula, outputs a bool: true if the input formula is a tautology and false if it is not.
Today we talked about sorting algorithms. We used cards to simulate several different sorting methods, and we wrote down the steps taken. We learned about insertion sort, quicksort, merge sort and bubble sort, and mentioned some others.
On the 10/05 we had the meeting with Guillermo. The companions explained the work they had done so far. After a pause, Gina, Martà and I explained to Guillermo what our practices consist of. Finally, Juan presented the idea of his master's tesis.
Today we talked about trees, specifically binary search trees. We saw how to implement them (and operations on them) in OCaml, and why they are useful for searching.
Today was the last class. We spent it finishing our homework with Ana's help, who gave us advice in some of the exercises we hadn't been able to do. Once finished, we did some of the exercites listed in the website https://ocaml.org/learn/tutorials/99problems.html . At last, we shared our impressions and opinions on this period of 'pràctiques' and we all agreed that it had been a very good, interesting and useful opportunity for us to learn the OCaml language and the work of Formal Vindications.