\not_specified #12
Comments
|
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?
* I have never used it explicitly.
* The default in a clause (in OpenJML anyway) is the same as omitting the clause.
* Without it, implementation is simpler
* Without it, explanation to the user is simpler
* Without it, we don't need to make a distinction between lightweight and heavyweight behaviors.
* A tool could supply something other than the standard default in place of \not_specified, but that would be better done by changing defaults across the board (to use inference, or some fixed set of defaults that is less conservative) rather than just where not_specified is implicit
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 GitHub<https://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 unsubscribe<https://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 iOS<https://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 Android<https://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>.
|
|
I also see There is also the |
|
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.
|
|
But we could also use comments in the stub contract generator, instead of |
|
Sure. I am happy with deprecating it. Keep the language small! |
|
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 :-)
|
|
Maybe we should clarify the default "expression", before we bury
|
|
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.
- David
… 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 <#12 (comment)>, 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>.
|
|
Resolved. |
|
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. |
|
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 <#12 (comment)>, 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>.
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Can we please deprecate \not_specified?
I have never used it explicitly.
The default in a clause (in OpenJML anyway) is the same as omitting the clause.
Without it, implementation is simpler
Without it, explanation to the user is simpler
Without it, we don't need to make a distinction between lightweight and heavyweight behaviors.
A tool could supply something other than the standard default in place of \not_specified, but that would be better done by changing defaults across the board (to use inference, or some fixed set of defaults that is less conservative) rather than just where not_specified is implicit
Is there a use case for it? It seems to me unneeded complexity/
The text was updated successfully, but these errors were encountered: