{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:56:03Z","timestamp":1750308963254,"version":"3.41.0"},"reference-count":10,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2004,2,1]],"date-time":"2004-02-01T00:00:00Z","timestamp":1075593600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2004,2]]},"abstract":"<jats:p>A temporal operator, namely leads-to, has been incorporated into the Dijkstra's weakest precondition calculus. It is demonstrated that the augmented calculus provides a basis, not only for the modeling but also, for a straightforward and thorough analysis of large and complex distributed systems. The technique has been illustrated by describing a data link layer protocol. This analysis contributes to the understanding of the system.<\/jats:p>","DOI":"10.1145\/967278.967282","type":"journal-article","created":{"date-parts":[[2005,11,14]],"date-time":"2005-11-14T18:08:27Z","timestamp":1131991707000},"page":"12-17","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Adding the leads-to operator to Dijkstra's calculus"],"prefix":"10.1145","volume":"39","author":[{"given":"Awadhesh Kumar","family":"Singh","sequence":"first","affiliation":[{"name":"National Institute of Technology, Kurukshetra, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anup Kumar","family":"Bandyopadhyay","sequence":"additional","affiliation":[{"name":"Jadavpur University, Kolkata, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_2_1_2_1","volume-title":"A discipline of programming","author":"Dijkstra E. W.","year":"1976","unstructured":"E. W. Dijkstra . A discipline of programming , Prentice Hall , 1976 . E. W. Dijkstra. A discipline of programming, Prentice Hall, 1976."},{"key":"e_1_2_1_3_1","volume-title":"Mathematical Logic for Computer Science","author":"Ben-Ari M.","year":"1993","unstructured":"M. Ben-Ari . Mathematical Logic for Computer Science , Prentice Hall , 1993 . M. Ben-Ari. Mathematical Logic for Computer Science, Prentice Hall, 1993."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1383-7621(00)00024-2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00033-B"},{"key":"e_1_2_1_6_1","first-page":"109","volume-title":"Proc. COMNAM-2000","author":"Bandyopadhyay A. K.","year":"2000","unstructured":"A. K. Bandyopadhyay . A mathematical model for the specification of data link layer protocols , In Proc. COMNAM-2000 , pages 109 -- 114 , December 2000 . A. K. Bandyopadhyay. A mathematical model for the specification of data link layer protocols, In Proc. COMNAM-2000, pages 109--114, December 2000."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_10_1","volume-title":"RVS group","author":"Henkel Dirk","year":"1999","unstructured":"Dirk Henkel . Safely sliding windows: Into the depths of formal system verification. Research Report , RVS group , Faculty of Technology, University of Bielefeld , April 1999 . Dirk Henkel. Safely sliding windows: Into the depths of formal system verification. Research Report, RVS group, Faculty of Technology, University of Bielefeld, April 1999."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647538.729711"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/967278.967282","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/967278.967282","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:38:19Z","timestamp":1750282699000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/967278.967282"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,2]]},"references-count":10,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,2]]}},"alternative-id":["10.1145\/967278.967282"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/967278.967282","relation":{},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2004,2]]},"assertion":[{"value":"2004-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}