syntax for representing specs of functions

[davidcok]

JML has accessible (reads) clauses for methods. These mostly use the same syntax as assignable clauses do.

//@ reads a, bar;
public int foo() { return a + bar; }

But if foo() calls a method, say bar(), then what?

• Do we list all the contents of all the reads clauses of all called methods, recursively? -- not very modular or maintainable
• Do we create a separate model field that contains the contents of bar()'s reads clause, so we can write

//@ model int _bar;

//@ reads _bar; or //@ reads b1, b2, b3; where b1 b2 b3 area all 'in' _bar
public int bar() { ... }
//@ reads _bar;
public int foo() { return bar(); }

---- also not very maintainable

• Or (my preference) do we add some syntax for designating the contents of a method's reads clause
  class A {
  //@ reads b1, b2. b3;
  public int bar() { ... }

//@ reads a, A::bar.reads;
public int foo() { return a + bar(); }

}

We could then also have A::bar.requires, A::bar.ensures, A::bar.assigns. (Dafny defines reads and requires like this)

Or a different syntax is possible: e.g. \requires(A::bar)
We'd want these to be applicable to lambda expressions also.

Thoughts?

[leavens]

Fundamentally, the read effect of a method should be handled like write effects, everything that a method's execution may read should be included in the accessible clause for that method, just like everything that a method may write must be included in the method's assignable clause. This kind of specification is modular, because the contract takes into account all the possible effects, the client does not need to know how the effect might be achieved in the code. This enables the client of a method to reason about a call to that method without having to look at the method's code or the specification of methods that it calls.

The use of data groups, pure methods, or location sets for tracking what a method is allowed to read can help with making the specification less burdensome to write and easier to maintain. I don't think that the specification of a method should refer to another method that the method in question calls, to me that is not modular, so I dislike the proposed syntax for designating the contents of another method's reads clause. Instead, I prefer the first solution that you say is not very maintainable, but which I think has no more maintenance problems than what we have for assignable (writes) clauses.

[davidcok]

Gary - I consider my first solution totally unworkable. One would need to list locations readable by a method own through all its call graph — which locations may not be known or even nameable by a method author. So that leads to with defining a datagroup for every method that reads anything, so that datagroup can be used in the reads clause of each of its callers. But that is a maintenance nuisance — we might as well implicitly define such a datagroup and have syntax for naming it. If you work through an example on paper, I think you will see what I mean. - David

…

On Feb 10, 2022, at 11:44 AM, Gary T. Leavens ***@***.***> wrote: Fundamentally, the read effect of a method should be handled like write effects, everything that a method's execution may read should be included in the accessible clause for that method, just like everything that a method may write must be included in the method's assignable clause. This kind of specification is modular, because the contract takes into account all the possible effects, the client does not need to know how the effect might be achieved in the code. This enables the client of a method to reason about a call to that method without having to look at the method's code or the specification of methods that it calls. The use of data groups, pure methods, or location sets for tracking what a method is allowed to read can help with making the specification less burdensome to write and easier to maintain. I don't think that the specification of a method should refer to another method that the method in question calls, to me that is not modular, so I dislike the proposed syntax for designating the contents of another method's reads clause. Instead, I prefer the first solution that you say is not very maintainable, but which I think has no more maintenance problems than what we have for assignable (writes) clauses. — Reply to this email directly, view it on GitHub <#48 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQBODBHHM3ECXRWIQVTU2PTPRANCNFSM5OBHZQAA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you authored the thread.

[leavens]

I don't see how doing that is any different than what we already do for assignable (writes) clauses. Are you talking about being able to have a method (say one far down the call chain) read some hidden cache or other private state?

[wadoon]

I can see the requirement to access elements in contracts, and other JML elements.

My thoughts are:

1. It should be in alignment to the typing rules of Java. Therefore obj::foo.ensures seems strange. obj::foo <: Supplier<T> and Supplier<T> does not have further member variables.
2. It should be in alignment with other specification access constructs. Currently, we have \invariant_for and \static_invariant_for.
3. We should also pay attention that there might be multiple contracts, but we can use their names. Also clauses can have names. For example, obj::foo.\contracts.<name>.ensures.\all to retrieve an expression (conjunction) of all ensures clauses in the contract <name>, and obj::foo.\contracts.<name>.ensures.myclause to retrieve a specific clause.
4. Maybe, we should think this further and maybe create a JML object system. Something I tried with the \spec namespace. For example, something like this:

Here is the uml code to play around:

@startuml
class java.Class {
}

class java.Method {}

class jml.Expression {}
class jml.Formula {}
class jml.Method {
  + visibility : VisibilityModifier
  + kind : {GHOST, MODEL}
  + name : String}
  + params : List<Parameters>
  + body : jml.BlockStmt
}

class jml.Field {
  + visibility : VisibilityModifier
  + kind : {GHOST, MODEL}
  + name : String
  + params : List<Parameters>
}


class jml.Class {
  +\inv : Formula
  +\initially : Formula
}

class jml.Contract {
  + name : String
  + assignable : Expression
}

jml.Contract -- "1..*" jml.FClause : +requires
jml.Contract -- "1..*" jml.FClause : +ensures
jml.Contract -- "1..*" jml.EClause : +diverges
jml.Contract -- "1..*" jml.EClause : +assignable

class jml.FClause {}
class jml.EClause {}

jml.EClause o-- "1..*" jml.Expression

java.Class --> "0..*" jml.Field
jml.FClause --> jml.Formula :  +/all
jml.FClause o-- "1..*" jml.Formula
java.Class --> jml.Class
java.Class --> "0..*" jml.Method
java.Method --> "0..*" jml.Contract
jml.Field --> "0..1" jml.Expression : "representsBy"
@enduml

[leavens]

Adding capabilities to refer to other specifications is a huge jump in expressiveness, and to my mind would make the specification language quite different than current JML. I am not sure of the properties of such a language and how verification tools could use it.

In addition, I worry about making a specification depend on the form of another specification, in ways that may break when the second specification is rewritten. For example, a JML specification like:

//@ requires P;
//@ ensures Q;
public void m();

could equivalently be expressed as:

 //@ ensures P ==> Q;
 public void m();

but this would have quite different interactions with the proposed constructs. Similarly using multiple specification cases is equivalent to a single specification case after some translation. So, it would make more sense if all specifications were transformed into some kind of normal form before access. Is that part of your proposal?

[mattulbrich]

I have two points:

1. Is there not a wellfoundedness problem:

class X {
   X x;

   //@ ensures next.foo::ensures
   void foo() { ... next.foo(); ... }
}

Probably we need something like a least/greatest fixpoint semantics here. I am confident that this can be chosen consistent, but it looks weird.

2. I agree with Gary that we should abstract from the inner workings of methods in modular verification.
   I have observed that in most cases it is the footprint of an object that one modifies. So having a ghost field "footprint" that lists all locations that belong to an object seems very sensible. So in most cases I would have: accessible / assignable this.footprint; Rarely I encounter arg.footprint for a method argument.

Sometimes one explicitly lists all fields, ok, but this is not really modular verification then.

[mattulbrich]

Actually, there is a way to abstract away from predicates / expressions canonically using model methods. Wojtek Mostowski and I have shown that at the Modularity 15 conference in Fort Collins, CO. (Gary was there 😄) https://link.springer.com/chapter/10.1007/978-3-319-46969-0_7

This can in particular be used in the face of subtyping. One can hand around a predicate o.preForMethodX() indicating that o satisfies the precondition for MethodX. In a modular context, one does not know how the predicate is defined, but one knows that it holds. And one can reason with it using dependency analyses.

No syntactical extensions needed. (We added "two_state" to abstract from post conditions and "\covariant" and "\contravariant" to ensure that predicates are reimplemented correctly.

[leavens]

I like the idea of using model methods to abstract from the specifications of other methods. (I will have to reread that paper...) And I like the idea that no syntactical extensions are needed.