I finished and marked the final exam for Structured Programming last week. I enjoyed teaching this course but I am very glad it's over. Perhaps surprisingly, considering the catastrophic results from my earlier exam, but the students in general did alright. Perhaps the poor performance shocked them into action somewhat and they practiced more. I also think I made the final exam a little gentler than the other assessments.

One thing that I regret doing, and will change in future iterations, is that the homework assignments (which I no longer trust as summative assessment, as they are solvable by LLM) did not have fixed due dates, but instead only recommended due dates before the exam/test for which they served as practice. The actual final due date was just at the end of semester, before the final exam I just marked. The result was, predictably in hindsight, that students didn't do the homework until the last minute, depriving them of the necessary programming practice before the midsession tests. We won't repeat this mistake.

Kai Phan has been building on her already very impressive result to produce a very nice picture of the monitorability landscape. I will present a brief summary of her results here, but eventually they will be incorporated into my research notebook on linear-time temporal properties. Mostly, our results concern the space of program properties — sets of program behaviours.

The classes of safety and guarantee above are the familiar closed and open sets respectively in the topology of program behaviours. In the above diagram, decision properties are the clopen sets — those sets that are both Safety properties and Guarantee properties, and obligation properties are, following Amir Pnueli, any boolean combination of closed or open sets.

Kai's original result was to show that all Bauer monitorable properties — that is, all properties for which a monitor can always potentially give an answer — cannot be distinguished from an obligation property by any monitor observing finite prefixes. What she has now done is prove that Bauer monitorable properties are exactly those properties that approximate an obligation property in this way. This led us to re-christen Bauer monitorability as the class of quasi-obligation properties. In a similar way, she has also identified the classes of quasi-safety and quasi-guarantee, which cannot be monitorably distinguished from safety and guarantee properties respectively, and proved that quasi-obligation properties are exactly those that are made up of boolean combinations of these.

At the bottom of the prism, we have another set of classes. What is commonly called weak monitorability sits at the very bottom — those properties for which there is at least one finite prefix that causes a monitor to give a definitive answer. We also have good monitorability and bad monitorability, which are those properties with at least one good or bad prefix respectively. It is easy to see that weak monitorability is the union of these classes. (Taking boolean combinations, as in the higher levels of the cube, leads to a trivial class containing all properties).

Kai has also now defined CTL characterisations for all of these lower classes, expressed as formulae over monitor trees, which we define reminiscent of Ghani, Hancock and Pattinson's stream processors. She then showed that the CTL formulae for all of the middle layer classes of the prism are obtained by wrapping the corresponding formula for the class below with \mathbf {AG}. For example, weak monitorability is defined as \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}), and quasi-obligation is just \mathbf {AG}\ \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}). Because of the aforementioned indistinguishability result (and because indistinguishable properties have indentical monitors), it's not possible to write CTL formulae for the top level of the prism, except for Decision properties (clopen sets) which correspond exactly to those monitors described by inductive trees — where all paths eventually terminate with an answer.

We're aiming to get this into ESOP or FoSSaCS this year. Hoping for the best! I think this is great work.

Dóminus illuminátio mea, et salus mea, quem timébo? Dóminus defénsor vitæ meæ, a quo trepidábo? Qui tríbulant me inimíci mei, infirmáti sunt, et cecidérunt.

Si iniquitátes observáveris Dómine, Dómine quis sustinébit? Quia apud te propitiátio est, Deus Israel.

Today at All Saints Ainslie we sang Palestrina's well-known Sicut Cervus:

Sicut cervus desíderat ad fontes aquárum:	Like as the hart desireth the waterbrooks:
ita desíderat ánima mea ad te, Deus.	So longeth my soul after thee, O God.

We didn't make any observation of the Sacred Heart, but that's not entirely unexpected for an Anglican parish, even a relatively spikey one.

Exáudi Dómine vocem meam, qua clamávi ad te: adiútor meus esto, ne derelínquas me neque despícias me, Deus salutáris meus.

Today at All Saints Ainslie we were in very reduced numbers — 1 to a part — but we sang Bob Chilcott's God so loved the world wonderfully!

God so loved the world

That he gave his only-begotten son

That whoso believeth in him should not perish

But have everlasting life.

Special thanks to Cindy Chen, our soprano soloist, and Mary-Anne Neilsen for stepping in and playing the organ at the last minute.