- cbc - software.imdea.org

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

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

2025

2024

2023

2022

2021

2020

cbc