ACSL++ manual

[vprevosto]

@davidcok I've rebased the branch and merged main.tex and main-cpp.tex, with a new mechanism to generate the various versions of the document that is less awkward than the sed-based approach that we used (see c378632). In addition, there is now a proper draft mode, in which the \TODO and \review comments will appear. Default is final mode to generate a proper manual (see 07bd0f5). Finally, I've fixed a few issues here and there, as mainly discovered by make check. Does it look OK for you?

[davidcok]

Hi Virgile. The master branch builds correctly for me — thanks for the overall organizational improvements. I will review the text of the documents for typos and formatting problems (and general improvements or corrections) later, but for now this is a good step forward.

• David

On Sep 20, 2019, at 2:58 AM, Virgile Prevosto notifications@github.com wrote:

@davidcok https://github.com/davidcok I've rebased the branch and merged main.tex and main-cpp.tex, with a new mechanism to generate the various versions of the document that is less awkward than the sed-based approach that we used (see c378632 https://github.com/acsl-language/acsl/commit/c378632778eaccc9392c78657173186bbc16c97e). In addition, there is now a proper draft mode, in which the \TODO and \review comments will appear. Default is final mode to generate a proper manual (see 07bd0f5 https://github.com/acsl-language/acsl/commit/07bd0f550070a2d7b92313425d146f084630c3de). Finally, I've fixed a few issues here and there, as mainly discovered by make check. Does it look OK for you?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQDHGBJZTEG5OLZE453QKRYCVA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7FY5FI#issuecomment-533434005, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQBZMKG5NUGUHTQRKY3QKRYCVANCNFSM4IYAIKOQ.

[vprevosto]

Hi Virgile. The master branch builds correctly for me

Maybe I wasn't clear enough, sorry. I haven't merged acslpp2 yet, so that if you want to check if everything builds fine, you have to be on this branch, not master.

[davidcok]

Hi - OK - not sure what I was seeing. But I looked at and pushed a few minor changes to the HEAD of acslpp2: 1) Adjusted format of cover and title page to accommodate line overflow in acslpp-implementation 2) The foreword pages (foreword.tex and cpp-foreword.tex) have an incorrect header. Apparently a \chapter* does not have empty header like a \chapter. In fact using \thispagestyle{plain} does not work either - so this slight problem remains. 3) I was seeing confusion in git between VERSION.tex and version.tex . I think I cleaned it up in favor of version.tex, but check that git is correct when you pull the change.

As I already said, I’ll read the bulk of the document for improvements later.

• David

On Sep 20, 2019, at 3:59 AM, Virgile Prevosto notifications@github.com wrote:

Hi Virgile. The master branch builds correctly for me

May be I wasn't clear enough, sorry. I haven't merged acslpp2 yet, so that if you want to check if everything builds fine, you have to be on this branch, not master.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQD7IT6OR65L3ZQ2HKDQKR7GFA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7F5ISA#issuecomment-533451848, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQCDYFUHVFABGGWF3ODQKR7GFANCNFSM4IYAIKOQ.

[vprevosto]

3) I was seeing confusion in git between VERSION.tex and version.tex . I think I cleaned it up in favor of version.tex, but check that git is correct when you pull the change.

Oops, I forgot about the uppercase version, and I guess that you have a case-insensitive file system that got a little bit confused at this point. Sorry about that. The current version.tex is fine anyway.

[vprevosto]

@jensgerlach What's your view on the current status of this branch?

[jensgerlach]

This comment refers to an another document

The examples in 0.11.2, 0.11.3, 0.11.4 are not legal C++ and rejected by a c++ compiler They look like Java code. Here are the compiler diagnostics for the Example in 0.11.2.

g++    -c -o A.o A.cpp
A.cpp:3:11: error: brackets are not allowed here; to declare an array, place the brackets after the
      name
int[] data;
   ~~     ^
          []
A.cpp:3:7: error: flexible array member 'data' with type 'int []' is not at the end of class
int[] data;
      ^
A.cpp:4:5: note: next field declaration is here
int data_length;
    ^
A.cpp:11:2: error: expected ';' after class
}
 ^
 ;

[vprevosto]

The examples in 0.11.2, 0.11.3, 0.11.4 are not legal C++ and rejected by a c++ compiler They look like Java code.

Good point. I'll amend the sources to have the examples in independent C++ files that can be checked for compilation errors in the same way we currently handle C examples

[jensgerlach]

On page 23

programming language type boolean

is mentioned. Does this refer to the programming language C++? In this case the name of the type is bool.

[jensgerlach]

Casts in ACSL and C are usually written as (type)object. In C++, the standard prefers imo writing type(object). Should this be reflected to ACSL++?

[jensgerlach]

In 2.3.3 (page 36), ACSL++ is mentioned in bold. Should this be set in green?

[jensgerlach]

In example 2.24 (page 42) there are no colons after the name of the behaviors.

Also on page 138. I recommend checking all behaviors.

[jensgerlach]

In section 2.4.3 (page 49, line 18 of the second code snippet) there is a \data.begin. I think the slash is wrong there.

I wonder, moreover, if the (corrected) expression

*(data.begin()+j))

makes sense in ACSL++, because operator * is here an overloaded version for list<int>::const_iterator

In my opinion this sections tries to cover to many things.

[jensgerlach]

I have noticed that the term receiver is used several times in the context of class methods. It's not to difficult to understand what is meant but I think this usage is not very common in the C++ community.

[vprevosto]

Good point. I'll amend the sources to have the examples in independent C++ files that can be checked for compilation errors in the same way we currently handle C examples

Done in 587a53e, 1fed27d, f265392, and 792bc90

[jensgerlach]

I have just noticed that I overlooked the description of \data in 2.4.3. Still, I think it's 'definition' and the long example is not so clear. Maybe one could start with the official defintion of range-based for which states that

for ( for-range-declaration : for-range-initializer ) statement 

is equivalent to

{
  auto &&__range = for-range-initializer ; auto __begin = begin-expr ;
  auto __end = end-expr ;
  for ( ; __begin != __end; ++__begin ) {
    for-range-declaration = *__begin;
       statement
  }
}

[jensgerlach]

Section 2.7.1. An example of a virtual predicate or logic function would be helpful.

[jensgerlach]

In the example of 2.7.6 could be a good place to use \this instead of this. I would also change the signature of

MyType operator+(MyType const& other);

to

MyType operator+(const MyType& other) const;

[jensgerlach]

In 2.7.8 I would change the signatures to

 C::C(const C&) = delete;
 C::C(const C&) = default;

[jensgerlach]

Section 2.7.7. talks about move constructors but I could not find any discussion of rvalue references X&&.

[jensgerlach]

Section 2.10.4

It would be clearer to me if

• hash_code is replaced by std::type_info::hash_code
• type_index is replaced by std::type_index

[jensgerlach]

2.11.2

The Array::getValue method should be declared as const

[jensgerlach]

2.11.3

The discussion of constexpr could be extended (it is only mentioned as a afterthought) in cluding an example.

[jensgerlach]

Page 82. There is a typo Inn particular

[jensgerlach]

2.9 Templates

What about templated predicates and logic functions?

[jensgerlach]

Section 2.9 speaks of parameterized template classes. Maybe parameterized classes suffices.

[jensgerlach]

Section 2.21.2. on class invariants is a bit vague. I thought one would mention here type invariants and their relationship to constructors, destructors and the other member function. I remember that we had quite some discussions about it.

[jensgerlach]

Page 113 mentions Jens !-)

[vprevosto]

On page 23

programming language type boolean

is mentioned. Does this refer to the programming language C++? In this case the name of the type is bool.

In fact, this remark contradicts a later discussion that says that you have an implicit conversion from bool to boolean but not the other way around, where you must be explicit. I'm just deleting this point.

[vprevosto]

Casts in ACSL and C are usually written as (type)object. In C++, the standard prefers imo writing type(object). Should this be reflected to ACSL++?

I'm adding a reference in the bnf for terms to the section where C++/ACSL++ casts are described in more details

[vprevosto]

In 2.3.3 (page 36), ACSL++ is mentioned in bold. Should this be set in green?

No, this is common to ACSL and ACSL++ and speaks about the semantics of the assigns clause.

[vprevosto]

I have noticed that the term receiver is used several times in the context of class methods. It's not to difficult to understand what is meant but I think this usage is not very common in the C++ community.

Indeed, the word receiver does not appear at all in the C++11 standard. I'll change the wording

[davidcok]

Sorry - though I did lots of C++ prior to Java’s invention, Java has been my primary language for a long time now.

Virgile — is there in place a make target to do the compile checking on these examples?

• David

On Sep 23, 2019, at 10:39 AM, Jens Gerlach notifications@github.com wrote:

The examples in 0.11.2, 0.11.3, 0.11.4 are not legal C++ and rejected by a c++ compiler They look like Java code. Here are the compiler diagnostics for the Example in 0.11.2.

g++ -c -o A.o A.cpp A.cpp:3:11: error: brackets are not allowed here; to declare an array, place the brackets after the name int[] data; ~~ ^ [] A.cpp:3:7: error: flexible array member 'data' with type 'int []' is not at the end of class int[] data; ^ A.cpp:4:5: note: next field declaration is here int data_length; ^ A.cpp:11:2: error: expected ';' after class } ^ ; — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQELHHIAAMPBVK7GC6LQLDII3A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7LCR4Y#issuecomment-534128883, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQHII6UMO6WLJMAJ67LQLDII3ANCNFSM4IYAIKOQ.

[davidcok]

Oops I see there is a Makefile addition for this purpose

On Oct 10, 2019, at 6:35 AM, David Cok david.r.cok@gmail.com wrote:

Sorry - though I did lots of C++ prior to Java’s invention, Java has been my primary language for a long time now.

Virgile — is there in place a make target to do the compile checking on these examples?

• David

On Sep 23, 2019, at 10:39 AM, Jens Gerlach <notifications@github.com mailto:notifications@github.com> wrote:

The examples in 0.11.2, 0.11.3, 0.11.4 are not legal C++ and rejected by a c++ compiler They look like Java code. Here are the compiler diagnostics for the Example in 0.11.2.

g++ -c -o A.o A.cpp A.cpp:3:11: error: brackets are not allowed here; to declare an array, place the brackets after the name int[] data; ~~ ^ [] A.cpp:3:7: error: flexible array member 'data' with type 'int []' is not at the end of class int[] data; ^ A.cpp:4:5: note: next field declaration is here int data_length; ^ A.cpp:11:2: error: expected ';' after class } ^ ; — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQELHHIAAMPBVK7GC6LQLDII3A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7LCR4Y#issuecomment-534128883, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQHII6UMO6WLJMAJ67LQLDII3ANCNFSM4IYAIKOQ.

[davidcok]

Actually, bool is the C++ type and boolean is the ACSL logic type (like int and integer).

• David

On Sep 25, 2019, at 7:06 AM, Virgile Prevosto notifications@github.com wrote:

On page 23

programming language type boolean

is mentioned. Does this refer to the programming language C++? In this case the name of the type is bool.

In fact, this remark contradicts a later discussion that says that you have an implicit conversion from bool to boolean but not the other way around, where you must be explicit. I'm just deleting this point.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQAYLBX6I6GZJE6FNWLQLNA25A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7RQDOI#issuecomment-534970809, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQAZPCIYUXV357W2PMTQLNA25ANCNFSM4IYAIKOQ.

[davidcok]

Text revised to note that the comment refers to both ACSL and ACSL++

On Sep 23, 2019, at 2:12 PM, Jens Gerlach notifications@github.com wrote:

In 2.3.3 (page 36), ACSL++ is mentioned in bold. Should this be set in green?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQGVDKK3TXXM3IQW7XDQLEBHBA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7LYQCY#issuecomment-534218763, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQBVBGT7DVWHF6XJ4EDQLEBHBANCNFSM4IYAIKOQ.

[davidcok]

Done.

On Sep 25, 2019, at 3:43 AM, Jens Gerlach notifications@github.com wrote:

Section 2.10.4

It would be clearer to me if

hash_code is replaced by std::type_info::hash_code type_index is replaced by std::type_index — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQEBBHCHHXHJBRN6WELQLMJAZA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q566A#issuecomment-534896504, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQAAIADR7LMYC5XTGXLQLMJAZANCNFSM4IYAIKOQ.

[davidcok]

Done,

On Sep 25, 2019, at 3:45 AM, Jens Gerlach notifications@github.com wrote:

2.11.2

The Array::getValue method should be declared as const

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQB2O3G6UMBGC2OO2STQLMJH7A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q6D6Y#issuecomment-534897147, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQGPQVTUNLTW47MQY3TQLMJH7ANCNFSM4IYAIKOQ.

[davidcok]

Fixed.

On Sep 25, 2019, at 3:48 AM, Jens Gerlach notifications@github.com wrote:

Page 82. There is a typo Inn particular

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQGB3KSX2LO7XK564GDQLMJU5A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q6NKA#issuecomment-534898344, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQEVWQA5RDCEW43JXR3QLMJU5ANCNFSM4IYAIKOQ.

[davidcok]

Actually - which would be preferable?
a) A distinction between bool and boolean, with casts required in some cases or b) A distinction, but no casts required or c) Equivalence - no casts and interchangeability.

I prefer (a) or (b) as it helps the reader remember to distinguish logic expressions from programming language expressions.

• David

On Sep 25, 2019, at 7:06 AM, Virgile Prevosto notifications@github.com wrote:

On page 23

programming language type boolean

is mentioned. Does this refer to the programming language C++? In this case the name of the type is bool.

In fact, this remark contradicts a later discussion that says that you have an implicit conversion from bool to boolean but not the other way around, where you must be explicit. I'm just deleting this point.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQAYLBX6I6GZJE6FNWLQLNA25A5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7RQDOI#issuecomment-534970809, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQAZPCIYUXV357W2PMTQLNA25ANCNFSM4IYAIKOQ.

[vprevosto]

Actually - which would be preferable? a) A distinction between bool and boolean, with casts required in some cases or b) A distinction, but no casts required or c) Equivalence - no casts and interchangeability. I prefer (a) or (b) as it helps the reader remember to distinguish logic expressions from programming language expressions. - David

I prefer a) as well (implicit conversion from C++ to ACSL++, cast required the other way around)

[davidcok]

Added some text and grammar material.

On Sep 23, 2019, at 2:10 PM, Jens Gerlach notifications@github.com wrote:

Casts in ACSL and C are usually written as (type)object. In C++, the standard prefers imo writing type(object). Should this be reflected to ACSL++?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQEO4DLANXJ7FOCADS3QLEBAHA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7LYKTY#issuecomment-534218063, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQGZAU56JGSFF6QLBGLQLEBAHANCNFSM4IYAIKOQ.

[davidcok]

Changed as suggested.

On Sep 25, 2019, at 3:28 AM, Jens Gerlach notifications@github.com wrote:

In the example of 2.7.6 could be a good place to use \this instead of this. I would also change the signature of

MyType operator+(MyType const& other); to

MyType operator+(const MyType& other) const; — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQHNK4LFCJ44W3BBFNLQLMHLBA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q43AI#issuecomment-534891905, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQDJXMHFX3ADEUZV65TQLMHLBANCNFSM4IYAIKOQ.

[davidcok]

Add an item in the TODO list, as this point will take some thinking and design.

On Sep 25, 2019, at 3:35 AM, Jens Gerlach notifications@github.com wrote:

Section 2.7.7. talks about move constructors but I could not find any discussion of rvalue references X&&.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQHA53X2XVLMKES4GXLQLMIFDA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q5MGI#issuecomment-534894105, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQGAZV4AMX7ZB5U46Y3QLMIFDANCNFSM4IYAIKOQ.

[davidcok]

Jens - are there particular issues you suggest be addressed? You likely are more familiar with uses of constexpr than I am.

• David

On Sep 25, 2019, at 3:47 AM, Jens Gerlach notifications@github.com wrote:

2.11.3

The discussion of constexpr could be extended (it is only mentioned as a afterthought) in cluding an example.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQGAUFTU6Y2HQVTXXV3QLMJQVA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q6KDA#issuecomment-534897932, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQFDHVTDJY5ROV5ZIKDQLMJQVANCNFSM4IYAIKOQ.

[davidcok]

I thought these were not necessary because ACSL already includes the ability to create logic type, functions and predicates with type parameters. There seems no need to replicate this in the C++ style.

Do you concur or not?

• David

On Sep 25, 2019, at 3:52 AM, Jens Gerlach notifications@github.com wrote:

2.9 Templates

What about templated predicates and logic functions?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQGODBT5EHEJOV5QOQ3QLMKCDA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q6WPA#issuecomment-534899516, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQA6ZDNRWZDKWGZLUFDQLMKCDANCNFSM4IYAIKOQ.

[davidcok]

And I added a grammar figure.

On Sep 25, 2019, at 7:12 AM, Virgile Prevosto notifications@github.com wrote:

Casts in ACSL and C are usually written as (type)object. In C++, the standard prefers imo writing type(object). Should this be reflected to ACSL++?

I'm adding a reference in the bnf for terms to the section where C++/ACSL++ casts are described in more details

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQCXMHHDNIK3M7XHI33QLNBRFA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7RQSFQ#issuecomment-534972694, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQANRJ2456WF7ZKB4E3QLNBRFANCNFSM4IYAIKOQ.

[davidcok]

In fact the problem is using the C++ variable data and the logic variable \data in the same example, as it leads to this confusion.

\data (and \count) are introduced as logic quantities to be able to state things that the program typically cannot.

I revised the example.

• David

On Sep 23, 2019, at 2:22 PM, Jens Gerlach notifications@github.com wrote:

In section 2.4.3 (page 49, line 18 of the second code snippet) there is a \data.begin. I think the slash is wrong there.

I wonder, moreover, if the (corrected) expression

(data.begin()+j)) makes sense in ACSL++, because operator is here an overloaded version for list::const_iterator

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQEOFZDXYD7NWBBV44LQLECPHA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7LZQIA#issuecomment-534222880, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQHLMEGDQ7Q7WCBMFC3QLECPHANCNFSM4IYAIKOQ.

[davidcok]

I’ll leave that point to be dealt with as the TODO items are resolved.

• David

On Sep 25, 2019, at 4:01 AM, Jens Gerlach notifications@github.com wrote:

Page 113 mentions Jens !-)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/64?email_source=notifications&email_token=ABITDQAQDUBPCKNUNP2X263QLMLGTA5CNFSM4IYAIKO2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7Q7QQI#issuecomment-534902849, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQEQKBTKLB6SCSUGDATQLMLGTANCNFSM4IYAIKOQ.