- cbc - CLIPLab

Installing Rodin
by Manuel Carro 14 Feb '23

14 Feb '23

It is very likely that we will start using Rodin in the next lecture (Wed, 16th). Therefore I ask you to follow the instructions at https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ and https://wp.software.imdea.org/cbc/#tools to download and install it. Please come to the lecture with laptops and batteries as full as possible (sometimes there are no cable extensions available, although I will try to have some of them in the lecture room). Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Welcome to Correctness by Construction
by Manuel Carro 29 Jan '23

29 Jan '23

Hi. If you receive this email, you have registered for the Correctness by Construction course. It is taught in three different master programs: MFII, EMSE, and MUSS, plus it is part of eligible requirements for the DSSC PhD program. The mailing list and the web page will be our primary communication means outside the classroom. The web page is located at https://wp.software.imdea.org/cbc/ and you can send messages to the mailing list using the address cbc(a)software.imdea.org Note that a message to the mailing list can reach *all* of your classmates. You are free to use it, but only for messages that should reach all of them. The mailing list uses the official mail addresses provided by the universities where you registered. Please make sure you read it frequently. Please let your classmates who are registered in CbC know that this message has been sent. The lectures will take place in the Montegancedo Campus of UPM every Wednesday from 4pm to 7pm at classroom 6306 (building 6, level 3, room 06). The first lecture will take place next Wednesday, February 1st. Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Slides / model for the lecture on May 11th
by Manuel Carro 15 May '22

15 May '22

Hi. I have just posted the material for the last lecture. Sorry it took so long, but I did not like that the material was half-cooked and I spent some time polishing the mode and the proofs, in the hope that it is ore useful. Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Extension for HW#3
by Manuel Carro 03 May '22

03 May '22

Dear all, I have received some requests to extend the deadline to turn in HW#3. However, a number of you have already submitted it, and it would be unfair to give a extension when some of you are / have been working on the homework, perhaps prioritizing it over other tasks. Therefore I believe that an adequate possibility would be as follows: - The deadline to turn in HW#3 is extended until Friday, May 6, 23:59. - The maximum grade, on a scale of 0 to 10, that can be obtained with this homework will be capped as follows: - If you turn it in by this Wednesday, May 4th, 15:59, you can have a maximum grade of 10 (out of 10). - Similarly, for Wednesday May 4th, by 23:59, the max. grade is 8.5. - Thursday May 5th, by 11:59: 7.0 - Thursday May 5th, by 23:59: 5.5 - Friday May 6th, by 11:59: 4.0 - Friday May 6th, by 23:59: 2.5 - Later than Friday May 6th, 23:50: 0.0 For example, if someone sends in the homework on Thursday at 10pm and the evaluation of the homework is an 8.0, the grade to be received would be 5.5. Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Term project
by Manuel Carro 02 May '22

02 May '22

Hi. The term project is available at https://wp.software.imdea.org/cbc/2022/05/02/project-term-robot-arms/ Important dates: - Deadline to send me the names of the group components: Wednesday, May 4th. - Deadline to send me the project material (please see the term project statement): Tuesday, May 24th, 23:59. - Presentation session: Wednesday, May 25th, 4pm to 7 pm. Best regards, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Plans for the rest of course
by Manuel Carro 27 Apr '22

27 Apr '22

Dear all, as we discussed today during the lecture, we will continue with Event-B during the rest of the course. I will make the term project available in short. The project is to be made in groups of *three* people and presented in a session. In order to free you as soon as possible and give you time to prepare other exams / homework, etc., we agreed to schedule the presentation of the project solutions for May, Wed 25th (approx. one month from now), in the same place and time slot we use for the lectures. Therefore: - If that date & time is NOT feasible for you, please let me know ASAP and, in any case, *before* next Wednesday (May 4). - Please set up groups of three people and send me (before next Wednesday) the names of the members of each group. If you are not able to make a 3-person group, please let me know ASAP (again, before next Wednesday) to look for a solution. Best regards, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Masks in lectures
by Manuel Carro 19 Apr '22

19 Apr '22

Dear all, as you may know, starting tomorrow, Wednesday 19th, the regulations regarding mask usage in Spain will be relaxed: they will not be mandatory in closed spaces (with a few exceptions). However, institutions and companies are free to require their use. UPM has decided to continue requiring the use of masks in its premises. So, please bring masks tomorrow to the lecture. Best, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Correctness by Construction: HW #3
by Manuel Carro 19 Apr '22

19 Apr '22

Hi. The third homework for Correctness by Construction is available at https://wp.software.imdea.org/cbc/2022/04/19/third-cbc-homework/ . The deadline to turn it in is May 4th, 2022. Best regards, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Lecture by zoom on Wednesday, April 6th
by Manuel Carro 05 Apr '22

05 Apr '22

Dear all, apparently a dysfunction in the heating system of the CS school, combined with the low temperatures in Madrid now, has forced the School to stop face-to-face lectures for the rest of the week. We have been asked to use Zoom / MS Teams instead. Therefore, tomorrow's lecture will be delivered via Zoom at the normal slot (4pm to 7pm). The coordinates are below: URL: https://zoom.us/j/5911012202 Password: CorByC Sorry about this late announcement -- I have just become aware of it. Best regards, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

Section 3.3 of HW #2 + extension
by Manuel Carro 01 Apr '22

01 Apr '22

Hi. I have received several questions regarding section 3.3 of HW2. Some of you have reasoned along the lines of "when the event Finish is enabled, then f(r) = y and we have found what we wanted". That is true, but it is not an answer. First of all, Finish might never be enabled; we never proved explicitly it was going to be enabled. Second, and more important: Finish is an artifact that appears in the model only to highlight a condition in which a sequential algorithm would have exited from a loop. But it does not do anything, and we may as well remove it and nothing changes in the model: all the proofs we discharged can still be discharged. So, let us assume that Finish does not exist and things will be clearer. Section 3.3 asks: how would you prove that IF the model eventually stops, then we will have found the location of 'v'? And I am asking you to find out a logic formula such that if it can be inferred from the axioms and the invariants, then the model eventually finds the location of 'v'. And, furthermore, you should be able to introduce this formula in Rodin as an invariant (perhaps marked as 'theorem') and, if Rodin discharges the formula, then you would have proved that the model eventually finds an r s.t. f(r) = v. Since this clarification is coming somewhat late, I will be accepting homework until Monday, April 4th, 23:59 without any penalty. Greetings, -- +-----------------------------------------------------------------------------+ | Manuel Carro --- E.T.S. Ing. Informáticos -- U. Politécnica de Madrid (UPM) | | Campus de Montegancedo --- E-28660 Boadilla del Monte --- Spain | | Phone: +34-91-101-2202 ext 4140 |

1 0

2026

2025

2024

2023

2022

2021

2020

cbc