- cbc - CLIPLab

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

Materials for the extra lecture of Mar. 27th
by Manuel Carro 27 Mar '21

27 Mar '21

Hi, all. The materials (slides, models, etc.) for the extra lecture we had yesterday is already online. 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

Extra lecture on Friday March 26th, 3pm-5pm
by Manuel Carro 26 Mar '21

26 Mar '21

Hello, everyone. We will finally have an extra lecture tomorrow, Friday 26th, from 3pm to 5pm. Please mark it in your agendas! Only three of you have not answered my request for comments on the extra lecture and, of them, only one apparently cannot possibly attend, while the other two can attend at least part of the lecture. Thanks to everyone. I will send you a zoom URL to connect as soon as I have 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 1

Reschedule for this Wednesday's lecture
by Manuel Carro 23 Mar '21

23 Mar '21

Hi, everyone. It will be impossible for me to give the whole CbC lecture this Wednesday; I have an unexpected meeting at 5pm which I cannot skip. I can still give a 50 min. session between 4pm and 5pm. I would like to reschedule the lecture (or, at least, part of it). Since there are students from three different programs (including Erasmus students), I do not know your schedule and I cannot propose a slot that I think may be reasonable for you. So, please find below a link to a doodle poll my availability for Thursday and Friday: https://doodle.com/poll/4bi4zxexcu928mtk?utm_source=poll&utm_medium=link Please fill it in as soon as you are able and, if possible, not later than tomorrow, Tuesday, 5pm. That will give me time to make a plan and everyone else to adjust accordingly. Best regards and thanks in advance for your response, -- +-----------------------------------------------------------------------------+ | 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 2

Yesterday's material, homework resubmission, theorems
by Manuel Carro 18 Mar '21

18 Mar '21

The material from yesterday's lecture is in the web site, including the one-way bridge model up to the point where we stopped. But please try to finish it with the material in the lecture on your own. Consult the model only if really necessary (because, e.g., things are really not working your you). Have it ready for next Wednesday, as we will continue working on it. Those of you who want to send me again first part of the first exercise sheet, please do so until next Wednesday *before the lecture*, so that I can quickly comment on the solutions next Wed. I cannot accept resubmissions after 4pm CET, Wed. 24th March. There was a question about the difference between theorems and non-theorems (in Rodin). From https://www3.hhu.de/stups/handbook/rodin/current/html/theorems.html: "Axioms, invariants and guards can be marked as theorems. This means that the validity of the theorems must be proven from the axioms, invariants or guards declared before the theorem." This definition does not shed light on why and when they are useful. First, an axiom/invariant/guard that is marked as a theorem can be used anywhere axioms/invariants/guards are used. Using them is sound if the theorem has been proved. The main corresponding PO is THM, and may involve other POs such as WD. The difference is how we prove a theorem vs. a non-theorem. An axiom marked as theorem has to be proved using the axioms (marked as theorem or no) *that appear before it*. On the other hand, a non-theorem axiom does not need a proof (but it may need e.g. WD POs): it is an initial truth. An invariant marked as a theorem has to be proven using the existing axioms (theorems or not) and the invariants (theorems or not) that appear before it. The INV PO is not necessary for theorem invariants, because they are derived from formulas that are invariants themselves. A guard marked as theorem can use all axioms and invariants plus the guards of the same event that appear before it. For example, in our one-way bridge model we may add the theorem guard "a + b + c ≤ n" and it will be discharged using the guards before it and the gluing invariant. Theorems can be used to: a) Have Rodin prove a specific property that is not a PO. For example, absence of deadlock is something that we may want or not. So we can write a formula that expresses it (as we did) and just "trick" Rodin into proving it by making it an invariant theorem which instructs Rodin to use whatever is available to prove it. It could as well be marked as a regular, non-theorem invariant. But in this case more proofs have to be done, because its establishment/preservation has to be proven for every event (5 proofs, in our case). If we mark it as a theorem, only one proof needs to be done, as it depends only on invariants and axioms. Of course not all invariant properties can be proven based on the rest of the invariants: some of them need to ensure that they are preserved across event activations. In the end, some invariant has to be the first one. b) Have pre-proved formulas that are useful in the proving process. That can happen because they often appear in manually-assisted proofs (as we hinted at with the use of f(i) > f(j) ⇒ i > j instead of i ≤ j ⇒ f(i) ≤ f(j) in the sorted array example), or because they are necessary to help automatic provers discharge some PO. In this sense they act as lemmas or auxiliary formulas in the CUT rule, which theorem provers don't use by themselves, but which we can simulate by introducing intermediate formulas (theorems) when we think it's appropriate. 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

2026

2025

2024

2023

2022

2021

2020

cbc