- cbc - CLIPLab

Second exercise sheet available
by Manuel Carro 14 Mar '21

14 Mar '21

The second Event-B exercise sheet is available. Please download it from https://wp.software.imdea.org/cbc/2021/03/14/826/ . Deadline: Friday, March 26 th 2021, 23:59. That is the last teaching day before Easter holiday. Please read carefully the exercise sheet. It is short but it is intended to contain all the information necessary. Pointers to more information are also included. Please follow them and read the associated information. Please do not procrastinate. The homework is not difficult and can be done quickly. But it one finds difficulties, it may need some time to try different strategies. Also, if you have not worked yet with Rodin, you will need some time to get used to the the editor and, more importantly, the interface with the theorem provers (the "proving perspective"). 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

On the definition of "sorted array"
by Manuel Carro 12 Mar '21

12 Mar '21

First of all, thanks to those who stayed on Wednesday for 15 additional min., and sorry for taking that extra time. I thought finishing that block was needed to start a new section next week. The lecture recording is already linked from the course webpage. When I asked for the specification of a sorted list, some of you suggested (1) ∀ i · [i ∈ 1..n-1 ⇒ f(i) ≤ f(i+1)] instead of (2) ∀ i,j · [(i ∈ dom(f) ∧ j ∈ dom(f) ∧ i ≤ j) ⇒ f(i) ≤ f(j)] IIRC, I said that both should be equivalent, but that I was not sure whether the first one could be directly used in the proof obligations. First of all, (1) is a particular case of the (2), and Rodin can prove that automatically: make (2) be an axiom and (1) a theorem; save, and should be proved. But the proofs use repeatedly the f(r) > v hypotheses, where v = f(x) for some x, so that we can use f(r) > f(x). That matches the contraposition of (2), but not that of (1), because we do not know the distance between r and x. So axiom (1) cannot be directly used. However, one "sees" clearly that if we have (1), then (2) should also be true. But that is because we in our minds apply (1) to position 1, then f(1) <= f(2); we repeat for f(2), then f(2) <= f(3) and therefore f(1) <= f(3), and so on. To really prove that this is the case, we have to find a formal proof. Proving *formally* that (2) can be inferred from (1) needs using an induction scheme similar (only similar -- I did not work it out, but it does not look straightforward) to P(0) ∧ ∀ n · n ∈ ℕ ∧ P(n) ⇒ P(n+1) for some arbitrary property P. This induction scheme is not part of the standard theorem provers available for Rodin, so it is not going to work out of the box. Such induction schemes *can* be written in Rodin, and we'll see an example if we have time. Bottom line: let's agree that (2) is a definition of a sorted list. Cheers, -- +-----------------------------------------------------------------------------+ | 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

Homework deadline - today 4pm
by Manuel Carro 10 Mar '21

10 Mar '21

This is a gentle reminder that the deadline to turn in the first homework expires in 4 hours. I have only received homework from ten of you so far. I have replied to all of them. If any of you sent me your homework and did not get a reply from me, please let me know (and, to make things easier for me, please resend it). Also, please remember *not* to forward your homework to the cbc(a)... list. It's very easy to hit "Reply All" by mistake. "Reply All" is in most cases the right option; but not in this particular situation! 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

Lecture this Wednesday, March 3
by Manuel Carro 01 Mar '21

01 Mar '21

Hi, everyone. As I mentioned during the last lecture, we will be using the Rodin tool this week. Please go to https://wp.software.imdea.org/cbc/rodin-installation-and-tips/ and follow the instructions there. Make sure your installation starts up. If it doesn't, please post _to this list_: if your question reaches other classmates, perhaps they can help you to find a solution. It'd be also great if you could familiarize yourselves with Rodin a bit, so that we are as agile as possible during the lecture: you will have to use the tool together with me. One final thing: I have a meeting from 3pm to 4pm this Wednesday. It may be the case that it takes some more time. In that case, I ask you to please wait for some minutes until I can join the Zoom room. Best, -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

CbyC: First homework
by Manuel Carro 25 Feb '21

25 Feb '21

The first homework for the Correctness by Construction course is available at https://wp.software.imdea.org/cbc/2021/02/25/first-event-b-homework/ 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

CbyC: slides & video
by Manuel Carro 11 Feb '21

11 Feb '21

Links to slides & video for Feb 10's session are available @ the course website (https://wp.software.imdea.org/cbc/). The password to access the video is the same we used for the zoom session. Best, -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Correctness by Construction: connection data for today's lecture
by Manuel 10 Feb '21

10 Feb '21

Hello everyone. The first lecture of the the Correctness by Construction course will take place today, February Wednesday 10, via Zoom. Please connect using the following data: https://zoom.us/j/9911012202 Password: CbyC Time: 4pm to 7pm The Zoom room will be available half an hour before the starting of the lecture in case you want to test your setup and make sure you can connect. I strongly advise to download the desktop application, rather than relying on the web-based interface. Please let you classmates know in case you think some of them is not reading / not receiving emails. 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

Correctness by Construction: connection data for today's lecture
by Manuel 10 Feb '21

10 Feb '21

Hello everyone. The first lecture of the the Correctness by Construction course will take place today, February Wednesday 10, via Zoom. Please connect using the following data: https://zoom.us/j/9911012202 Password: CbyC Time: 4pm to 7pm The Zoom room will be available half an hour before the starting of the lecture in case you want to test your setup and make sure you can connect. I strongly advise to download the desktop application, rather than relying on the web-based interface. Please let you classmates know in case you think some of them is not reading / not receiving emails. 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

Anonymous Doodle created and sent
by Manuel Carro 27 May '20

27 May '20

Dear all, you should have received three emails from no_reply(a)doodle.org with a link to vote for the presentations made by each other group -- please check your 'spam' folder in case they have been stored there. The deadline to vote is until tomorrow afternoon. The poll results cannot be observed until then. Thanks for your collaboration! Best, -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

Today's session
by Manuel Carro 27 May '20

27 May '20

Hi. I think I had not sent you the links for today's session: https://zoom.us/j/7911012202 Passwd: 26404152 Again, from 3pm to 6pm. See you! -- Manuel Carro : manuel.carro(a){imdea.org,upm.es} Director, IMDEA Software Institute : http://software.imdea.org Associate Professor, School of CS, UPM : http://www.fi.upm.es EIT Digital Spain : http://www.eitdigital.eu Madrid, Spain : +34-91-101-2202 ext. 4140

1 0

2026

2025

2024

2023

2022

2021

2020

cbc