search

JavaModelingLanguage / RefMan

4 stars 0 forks source link

\not_specified #12

Closed davidcok closed 2 years ago

davidcok commented 2 years ago

Can we please deprecate \not_specified?

Is there a use case for it? It seems to me unneeded complexity/

leavens commented 2 years ago

Hi David and all,

Yes, I agree that it is fine to deprecate \not_specified, as long as we have a discussion about defaults somewhere in the reference manual. The idea was to provide a way to explicitly discuss and call for the defaults, for whatever tool one was using, and we thought that the defaults might be different between RAC and ESC.

I am also okay with getting rid of the distinction between lightweight and heavyweight specifications. Originally the idea was that lightweight specifications were partial ones, more suited for RAC in the design by contract (DbC) style and that heavyweight specifications were more complete and better suited to ESC and static verification. But I agree that we aren't really making that distinction much in practice.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

From: David Cok @.> Sent: Wednesday, December 8, 2021 9:56 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: [JavaModelingLanguage/RefMan] \not_specified (Issue #12)

Can we please deprecate \not_specified?

Is there a use case for it? It seems to me unneeded complexity/

- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FJavaModelingLanguage%2FRefMan%2Fissues%2F12&data=04%7C01%7CLeavens%40ucf.edu%7C99a75867848a4c0cd3cf08d9ba5acd83%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745721430877467%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=GK2GyedQQGb7iLAEVMGAUS05gg8DIJJzBGR0IX0tbIA%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPONNROX5LJLSTS2HZLUP5WWZANCNFSM5JUACPJQ&data=04%7C01%7CLeavens%40ucf.edu%7C99a75867848a4c0cd3cf08d9ba5acd83%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745721430887463%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=VrIPDzJCQ1nXmyXnBrzmOeu5dZijFSWf9ExTX38TKyc%3D&reserved=0. Triage notifications on the go with GitHub Mobile for iOShttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7CLeavens%40ucf.edu%7C99a75867848a4c0cd3cf08d9ba5acd83%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745721430887463%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=0tm1ocOqagDC9W%2F7D8qytcaof9YLOMFur1YgLTaJDiU%3D&reserved=0 or Androidhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7CLeavens%40ucf.edu%7C99a75867848a4c0cd3cf08d9ba5acd83%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745721430897462%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=oY5t411ycTT9N0xMgmKNAXT60Dh6qopS2m6mm1Krvtg%3D&reserved=0.

wadoon commented 2 years ago

I also see \not_specified as deprecated for the use by user. It might still be useful for implementors of JML when building the JML (meta-)model.

There is also the \same keyword. Do you also want to deprecate it?

mattulbrich commented 2 years ago

I think KeY supports it.

I think there is a jml editor tool somewhere in our repository which seems to generate

/*@ public normal_behavior
   @  requires \not_specified;
   @  ensures \not_specified;
   @  assignable \not_specified;
   @*/

which sounds sensible. Could it not mean that these clauses behave as if not specified.

wadoon commented 2 years ago

But we could also use comments in the stub contract generator, instead of \not_specified

/*@ public normal_behavior
   @  //requires expr;
   @  //ensures expr;
   @  //assignable locset;
   @*/
mattulbrich commented 2 years ago

Sure. I am happy with deprecating it. Keep the language small!

leavens commented 2 years ago

Hi Mattias and all,

So we all seem to agree on this.

(As to "keeping" the language small, I think it's a bit late for that, but "making the language smaller" is sensible.)

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

From: Mattias Ulbrich @.> Sent: Wednesday, December 8, 2021 10:43 AM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] \not_specified (Issue #12)

Sure. I am happy with deprecating it. Keep the language small!

- You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FJavaModelingLanguage%2FRefMan%2Fissues%2F12%23issuecomment-988927825&data=04%7C01%7CLeavens%40ucf.edu%7C31c0c6b7e3cb482f536d08d9ba616954%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745749812959733%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=E53FkXC7tbQ5HgShz3d3NzodanZ95JFIjNQiGIDAjrI%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPN3FHRYZK5N35UMGLDUP54IFANCNFSM5JUACPJQ&data=04%7C01%7CLeavens%40ucf.edu%7C31c0c6b7e3cb482f536d08d9ba616954%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745749812969723%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=2MIcsLxOraSALtUUkc9SH8dpRRTDCkIKk9WyM41GPaE%3D&reserved=0. Triage notifications on the go with GitHub Mobile for iOShttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7CLeavens%40ucf.edu%7C31c0c6b7e3cb482f536d08d9ba616954%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745749812979723%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=UD%2BMjpD6F9Cok4T2n0Ywt596A58KhLkmquDnpVDlx24%3D&reserved=0 or Androidhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7CLeavens%40ucf.edu%7C31c0c6b7e3cb482f536d08d9ba616954%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637745749812979723%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ElWiXYbXr2zggdi153c8INSVWGRqr6L%2F6pa1fQ87xT8%3D&reserved=0.

mattulbrich commented 2 years ago

On 08.12.21 16:47, Gary T. Leavens wrote:

(As to "keeping" the language small, I think it's a bit late for that, but "making the language smaller" is sensible.)

It's more work, but as prudent I think :-)

wadoon commented 2 years ago

Maybe we should clarify the default "expression", before we bury \not_specified. A contract without an requires clause, has the following implicit value as the pre-condition:

  1. true,
  2. inherits its pre-condition (from contract of the overridden method),
  3. a tool-specific default.
davidcok commented 2 years ago

Each kind of clause has a default if omitted. This is the same default. In rewriting the RM I’m making sure those are clear. For now the JML default is (1) in this case. However, tools are welcome to implement options (e.g., -infer) that might infer better expressions for instated clauses. In fact I’d like to get to that sometime…

We’ll call this issue closed.

On Dec 8, 2021, at 10:57 AM, Alexander Weigl @.***> wrote:

Maybe we should clarify the default "expression", before we bury \not_specified. A contract without an requires clause, has the following implicit value as the pre-condition:

true, inherits its pre-condition (from contract of the overridden method), a tool-specific default. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/JavaModelingLanguage/RefMan/issues/12#issuecomment-988940779, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABITDQARCSVZHD3CWTOUP3DUP555DANCNFSM5JUACPJQ. 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.

davidcok commented 2 years ago

Resolved. \not_specified is deprecated. Where it would have been explicitly used, just omit the clause The clauses all have defaults if they are omitted. This also lessens the cognitive distance between lightweight and heavyweight behaviors, such that we won't continue to make that distinction (though the different kinds of behaviors do have some different defaults). A lightweight behavior is just a regular 'behavior' with the visibility of the associated method.

mattulbrich commented 2 years ago

For the record: Let's keep well-defined default clauses for now and talk about inferences and their impact on defaults later. I am skeptical.

davidcok commented 2 years ago

Certainly — that is very much in the future — just making the point that it is a conceivable option

On Dec 8, 2021, at 11:05 AM, Mattias Ulbrich @.***> wrote:

For the record: Let's keep well-defined default clauses for now and talk about inferences and their impact on defaults later. I am skeptical.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/JavaModelingLanguage/RefMan/issues/12#issuecomment-988948472, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABITDQHFU6GX63TU3PSVFCLUP5635ANCNFSM5JUACPJQ. 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.