{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T15:08:53Z","timestamp":1745334533243},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T00:00:00Z","timestamp":1491264000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,6]]},"abstract":"<jats:p>A semigroup-based setting for developing Hoare logics and refinement calculi is introduced together with procedures for translating between verification and refinement proofs. A new Hoare logic for multirelations and two minimalist generic verification and refinement components, implemented in an interactive theorem prover, are presented as applications that benefit from this generalisation.<\/jats:p>","DOI":"10.1017\/s096012951700007x","type":"journal-article","created":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T08:46:20Z","timestamp":1491295580000},"page":"775-799","source":"Crossref","is-referenced-by-count":4,"title":["Hoare Semigroups"],"prefix":"10.1017","volume":"28","author":[{"given":"GEORG","family":"STRUTH","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,4,4]]},"reference":[{"key":"S096012951700007X_ref6","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"S096012951700007X_ref3","first-page":"197","volume-title":"ITP","author":"Armstrong","year":"2013"},{"key":"S096012951700007X_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"S096012951700007X_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.002"},{"key":"S096012951700007X_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/23005.23008"},{"key":"S096012951700007X_ref5","first-page":"19","article-title":"Reasoning about imperative quantum programs","volume":"158","author":"Chadha","year":"2006","journal-title":"ENTCS"},{"key":"S096012951700007X_ref4","unstructured":"Armstrong A. , Struth G. and Weber T. (2013b). Kleene algebra. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/entries\/Kleene_Algebra.shtml."},{"key":"S096012951700007X_ref1","unstructured":"Armstrong A. , Gomes V.B.F. and Struth G. (2014). Kleene algebra with tests and demonic refinement algebras. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/entries\/KAT_and_DRA.shtml."},{"key":"S096012951700007X_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_7"},{"key":"S096012951700007X_ref8","doi-asserted-by":"crossref","first-page":"30:1","DOI":"10.1145\/2785967","article-title":"Concurrent dynamic algebra","volume":"16","author":"Furusawa","year":"2015","journal-title":"ACM TOCL"},{"key":"S096012951700007X_ref13","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"S096012951700007X_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.05.007"},{"key":"S096012951700007X_ref12","volume-title":"Programming from Specifications","author":"Morgan","year":"1994"},{"key":"S096012951700007X_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"S096012951700007X_ref15","first-page":"180","volume-title":"ITP 2013","author":"Pous","year":"2013"},{"key":"S096012951700007X_ref2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s00165-015-0343-1","article-title":"Building program construction and verification tools from algebraic principles","volume":"28","author":"Armstrong","year":"2016","journal-title":"Formal Aspects of Computing"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951700007X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,14]],"date-time":"2019-04-14T15:41:23Z","timestamp":1555256483000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951700007X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,4]]},"references-count":16,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["S096012951700007X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951700007x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,4]]}}}