- cbc - software.imdea.org

Event B: Term Project
by Manuel Carro 05 May '21

05 May '21

Hi, all. I have just posted the Event B term project, which some of you asked me about. In order for you to have time enough to work on it, the presentation dates have been moved one week forward. That also makes Wed. May 19th available in case it is needed to complete material from the 2nd part of the course. Therefore, in principle you should be able to finish with the course duties either on May 26th or on June 2nd, depending on when you do your presentation. Please go to https://wp.software.imdea.org/cbc/2021/05/05/event-b-term-project/ to see the deadlines and access the project description and how to turn it in. As always, please drop me a line in case you have question / doubts. 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

First set of exercises for part II
by Manuel Hermenegildo 04 May '21

04 May '21

Dear all, I have posted some exercises corresponding to the material of the first lecture. For now please try to do the exercises and have at least some of them ready for the next class (May 5). You will have to turn them in eventually, combined with the following set of exercises, that will be sent after the next class. Cheers, Manuel -- ------------------------------------------------------------------------- Manuel Hermenegildo manuel.hermenegildo(a)imdea.org -------------------------------------------------------------------------

1 0

Graphical interface with Ciao
by Quico del Real 29 Apr '21

29 Apr '21

Dear everyone, Is there a way to have a graphical interface for the ciao prolog program? I don’t use the terminal very often so I’m struggling with getting to know how to use it. Is there a guide of shortcuts for the terminal? Regards, Quico

4 4

Lightning talks (offtopic)
by Manuel Carro 29 Apr '21

29 Apr '21

Hi! This message is unrelated to the CbC lectures, but it may be interesting for some of you. The ACM chapter of the UPM organizes a series of Lightning Talks every semester. They are broadcast through twitch.tv at https://www.twitch.tv/acmupm . There is a talk session tomorrow, Friday 30th, at 5pm (see one announcement here: https://twitter.com/acmupm/status/1387696757795139588?s=20). I was asked to give a talk, and I think that if you found the Correctness by Construction course minimally interesting, you may find my talk interesting, too! I won't advance the topic, but its title is "Truths I will never tell you". The only thing is that it will be in Spanish, so unless you have a minimal proficiency, you may not get much from it... Best regards, -- 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

slides, examples, and recordings posted
by Manuel Hermenegildo 29 Apr '21

29 Apr '21

Dear all, the slides, the files with the examples used in class, and the recordings of today's class have now been posted on the web site. Cheers, Manuel -- ------------------------------------------------------------------------- Manuel Hermenegildo manuel.hermenegildo(a)imdea.org -------------------------------------------------------------------------

1 0

Start of second part and Ciao installation
by Manuel Hermenegildo 28 Apr '21

28 Apr '21

Dear all, this is a gentle reminder that with tomorrow's class we start the second part of the Correctness by Construction course. In this part the main tool we will be using is Ciao. I have left relevant information about Ciao on the course web site, including installation instructions and pointers to documentation. I you can have Ciao installed in your computer for this first class, you can try examples already during the class, but it is not strictly necessary. It will be necessary however to do the exercises and to be able to follow the second and third classes. Look forward to seeing you tomorrow. Cheers, Manuel -- ------------------------------------------------------------------------- Manuel Hermenegildo manuel.hermenegildo(a)imdea.org -------------------------------------------------------------------------

1 1

Homework Q & A / Rodin 3.6
by Manuel Carro 13 Apr '21

13 Apr '21

Hi. You may have questions re. the CbC homework #3. If so, and in order not to take time from tomorrow's lecture, I propose the following: I can connect to the Zoom room ahead of time (say, 15:30 tomorrow) and stay a bit longer (until, let us say, 19:30). This way we do not have to use email, which may be somewhat slow, or set up an appointment. If any of you plan to to use any of these slots, please let me know so that I connect before the lecture / know I should stay after it. On a different topic, I have been using Rodin-3.6-RC1 (the release candidate for version 3.6) for a couple of weeks now and it is working well. Some of the edition bugs in the 3.5 version have disappeared and I think it is stable enough to be used regularly. If you want to give it a try, you can download it from https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/ When you start a new Rodin version for the first time, it asks for the location of the workspace to use. If it was created by a previous version, it is updated. I am not sure it can be used by a previous Rodin version after this update. So I recommend making a backup of the Rodin workspace before starting 3.6 in case things go wrong and you need to backtrack. Cheers, -- 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

Reminder: no lecture today
by Manuel Carro 07 Apr '21

07 Apr '21

Reminder: there is no lecture Correctness by Construction lecture today, as UPM has Monday lectures to compensate for several Mondays that are holidays during this semester. 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

Third Event-B Homework: Room for One
by Manuel Carro 03 Apr '21

03 Apr '21

The third homework for Event-B is available. Deadline: Wednesday, April 21st, 15:59. Please access it at https://wp.software.imdea.org/cbc/2021/04/03/third-event-b-homework/ 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

Proving tips
by Manuel Carro 29 Mar '21

29 Mar '21

Some of you asked me for advice on how to prove with Rodin. There are some tips in the slides and in documents linked from the course web, but I thought I could put together what I think may be useful recommendations. Please find them at https://wp.software.imdea.org/cbc/proving-tips/ Best / Saludos, Manuel -- +-----------------------------------------------------------------------------+ | 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