\hence_by

[davidcok]

Gary - the old DRM says

The hence_by statement is used to record reasoning when writing a proof by intermittent assertions. It would normally be used between two assert statements (see section 13.3 Assert Statements) or between two assume statements (see section 13.4.1 Assume Statements).

In actual practice, how would this be different than just assuming the hence_by expression? In both cases the expression would be some tautology that the solver can't figure out on its own. hence_by has the same soundness problems as assume. Is there a connotation difference that recommends a distinct name?

[ We should find a better word than 'intermittent' ] (@leavens)

[wadoon]

I am not sure whether we should keep \hence_by in the ref manual, as it is just support for the verification tool. In a different issue, we had the tendency against proof commands and hints in JML.

On the other side, I would love to have a language in which I can explain to KeY why I am right, and hence the program is correct. But further research are required to get there.

[leavens]

Hi Alexander, David, Mattias,

Yes, I agree that, following what I said earlier about not recording proof details, we should probably delete hence_by from JML. I doubt that anyone will miss it.

    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: Alexander Weigl @.> Sent: Monday, December 13, 2021 7:21 PM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Mention @.> Subject: Re: [JavaModelingLanguage/RefMan] \hence_by (Issue #24)

I am not sure whether we should keep \hence_by in the ref manual, as it is just support for the verification tool. In a different issue, we had the tendency against proof commands and hints in JML.

On the other side, I would love to have a language in which I can explain to KeY why I am right, and hence the program is correct. But further research are required to get there.

- You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FJavaModelingLanguage%2FRefMan%2Fissues%2F24%23issuecomment-993032908&data=04%7C01%7CLeavens%40ucf.edu%7C1f5a77a2bb304c91888908d9be97a055%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750380706274516%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=Jgj8sg0OajgvpzjBPRBQv%2FF0Zd4ucMr%2Bk7%2F1F%2BQPsII%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPOUAT2HI7I3SVMERHTUQ2EXJANCNFSM5J63FYFQ&data=04%7C01%7CLeavens%40ucf.edu%7C1f5a77a2bb304c91888908d9be97a055%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750380706284508%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=4kXHin3hLph0oglHXNBNeraPXHElpNixvnHcedjqqCE%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%7C1f5a77a2bb304c91888908d9be97a055%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750380706284508%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=Fnl%2BiFK0WNZ4Ulg0hjx4%2FMsj0xWhRuLvvmiKJfTmNbw%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%7C1f5a77a2bb304c91888908d9be97a055%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750380706294501%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=PDsnDTGgcMzl11bca3q4H78Wa%2FbSgvvRxmgHHriFWzI%3D&reserved=0.

[davidcok]

OK. Resolved. hence_by is deprecated. You can use assume to help a proof along if you want.