cbc February 2020

cbc@software.imdea.org

2 participants
5 discussions

Yesterday's session
by Manuel Carro 27 Feb '20

27 Feb '20

This is a followup to yesterday's session, especially for those who could not attend the 2nd half. We finished correcting most of the homework and we devoted part of the session to model the exercises in Rodin. We had time to do the "Odd way" to calculate n^2 only, as we bumped into some technical hurdles. I believe that the mail Ignacio sent sheds light on how to solve the problem. Please howl if that is not the case. For those who attended the full lecture: please model on your own the Russian multiplication in Rodin, including correctness and termination (as we did in th "Odd n^2". Note: Rodin has 'mod' among the arithmetic operators. Some invariant may not be proven straight away. Nothing to worry about, and this it can be different for each of you. There are reasons for that - more on it in the next session and the cure is easy. For those who did not do that last part: *please* make sure to install Rodin as per the instructions in the last set of slides, import the IntegerDivision example to see what a model and the editor looks like, and try to model the n^2 and the Russian multiplication calculations. In the next session I plan to show something with the Russian multiplication example and I would like you to be up-to-date with it. And in coming sessions ad homeworks I plan you to use Rodin extensively. Rodin can be initially disconcerting, but it is only 10 minutes until one understands how the editor works. I suggest that your pair up with some of your classmates for a quick primer. Ask in the mailing list if you experience problems. 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

Problems with automatic proving in Rodin
by Ignacio Ballesteros 26 Feb '20

26 Feb '20

Hi! At the end of the class some of us were having problems with automatic proving in Rodin. We were supposed to have installed Rodin Version: 3.4.0 and then install Atelier B Provers through "Help > Install New Software". I did that steps but it didn't work, Proof Obligations were still in brown. I just tried to install again Atelier B Provers, and this time, a popup appear after agreeing terms of service asking if "I was really sure to install that software". This popup didn't appear in previous installations. After accepting (and a suggested restart), proofs were passing. I don't know if this may be a solution for the ones who also have this same problem, but maybe double-checking that Atelier is installed can help. Ignacio. Just to make sure, these are my software versions: - Linux 5.5.5-arch1-1 _Name Version Id Provider_ Atelier B provers 2.2.1.r16701 com.clearsy.atelierb.provers.feature.group ClearSy Rodin Handbook v.2.5 2.5.0.201606291411 org.rodinp.handbook.feature.feature.group Formal Mind GmbH Rodin Platform 3.4.0.201802230927-6980ca1 org.rodinp.platform.product null Event-B Modeling Environment 3.4.0.201802230927-6980ca1 org.eventb.ide.feature.group ETH Zurich Rodin Platform Feature 3.4.0.201802230927-6980ca1 org.rodinp.platform.feature.group ETH Zurich You can make sure of installed versions going to "Help > About Rodin Platform > Installation Details"

2 1

Reminders for tomorrow
by Manuel Carro 25 Feb '20

25 Feb '20

Hi. This is a reminder for tomorrow's lecture: - The first homework is due tomorrow @ 3pm. Send me PDFs by mail. Scans of hand-written papers is OK. You can also hand me a physical page, but then you won't keep a copy. - Make sure you have a working Rodin installation. Refer to the slides at https://wp.software.imdea.org/cbc/wp-content/uploads/sites/5/2020/02/03-1-s… and follow the instructions in the section "Rodin: the Event B modeling tool". - Bring a laptop with Rodin working, because I intend for you to use it in class. Best, 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

Material & next lecture
by Manuel Carro 13 Feb '20

13 Feb '20

Hi. I have left at https://wp.software.imdea.org/cbc/ ("Course Log" section) the material for the last lecture, plus homework (to be turned in by Wed., Feb 26th, 3pm). More people have joined the lectures, and we won't fit in the meeting room we were using. Therefore, next Wednesday's lecture will take place in meeting room 302 (same level, in the corner by the kitchen). See you there. -- 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

Tomorrow's lecture
by Manuel Carro 11 Feb '20

11 Feb '20

This is a reminder that tomorrow we'll have a lecture again @ the IMDEA Software Institute, room 379, from 3pm to 6pm. If you bring a mug I'll treat you to coffee or tea (we try not to generate waste). 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

2025

2024

2023

2022

2021

2020

cbc February 2020