Review CH 1&2

[davidcok]

Please read and review this preface and introductory chapters. You can do so in Overleaf but I've attached them if that is easier. Ignore the blue notes page.

Gary - in particular make sure that the history and acknowledgements are up to date.

Also, I've turned on back references from the bibliography back to the page containing the internal \cite command. With that, do you think we still should have authors of cited papers listed in the index?

IntroMaterial.pdf

[mattulbrich]

I have left a few detail comments in overleaf. (fixed a few rare typos without comment.)

I wonder if "behavior" is the same as "contract" in design-by-contract. That link should be established.

I think the description of what a behaviour comprises on p 3 is still a little rough. I made a few suggestions (in overleaf)

[davidcok]

Gary - as many of MU's comments are on material taken from the DRM, please consider those (search for mutodo in Overleaf) when you get to reviewing this

[leavens]

I have reviewed chapters 1 and 2 and updated the history and acknowledgments as best I could.

[davidcok]

Going over the comments on Preface/Ch1/Ch2:

• Mattias asked if the example belonged here. Although it is not necessary, I think it is a useful part of the introduction. To me concrete examples are always useful in theoretical settings. All agree?

• Ch1 uses a lot of lstinline snippets -- which makes for a mix of bold face for keywords (like requires) and texttt for program identifiers. Are we OK with this? Or shall I change it all to text style? (I'd keep the lstlisting use of bold keywords in the displayed program code in any case) ---- My preference - no keyword highlighting inline -- too many fonts

• A comment says that 'frame axiom' is a usual term. However, I'd prefer 'frame condition' for its similarity to 'precondition' and 'postcondition', and 'frame condition' is used elsewhere.

• Mattias: should the acknowledgments include anything regarding the KeY team or its funding? I put in "Contributions of Mattias Ulbrich stem from his participation in the \KeY project. Other members of that team, such as Alexander Weigl, also contributed comments, language suggestions and critiques." but please suggest your own text or that it be omitted.

• Gary - I find including names of authors of cited works in the index to be unusual. I have enabled back like (with page numbers) from the bibliography to the text. Is that sufficient? Or would you rather keep the author's names in the index? Your call.

[leavens]

• I agree it's useful to have an example in the introduction. And in general I do agree that concrete examples can help make theoretical discussions clearer, like the example in chapter 1.
• I like the keyword highlighting, so I would prefer that we use a style that makes that happen in the examples.
• I'm okay with either frame axiom or frame condition; we should just be consistent.
• I like having the authors names mentioned in the text in the index, that way people can look themselves up. But if it's too much work, we can omit it (but then we should take out all the old ones).

[davidcok]

OK, except " I like the keyword highlighting, so I would prefer that we use a style that makes that happen in the examples."

In the examples its fine. It when keywords are just mentioned in the text, but put in code font that to me the differing presentation of keywords and other code becomes distracting to reading.

[davidcok]

And @mattulbrich - are the acknowledgments OK?

[mattulbrich]

• I prefer keyword highlighting in text, as it ensures that ensures is always understood correctly :grin:
• frame condition: a condition (or axiom) sounds like a Boolean expression to me. What exactly is the framing condition? For me that condition is the knowledge that a value has not changed if a method has been called. If you specify assignable X the X would not be a frame condition (as it not a condition).
• Let me check with the acknowledgements. We have a DFG-funded project on KeY and making it more accessible and that could and should be mentioned, I assume. (No hurry, I assume?)