{"entities":{"Q1106014":{"pageid":1116763,"ns":120,"title":"Item:Q1106014","lastrevid":66449811,"modified":"2026-04-12T10:09:32Z","type":"item","id":"Q1106014","labels":{"en":{"language":"en","value":"A proof system for distributed processes"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4060689"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$95E2E3FE-E10B-43FF-8834-09FF233C58B5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b0fb8c89efe48e9a55a89059536ae3fc9962201d","datavalue":{"value":{"text":"A proof system for distributed processes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1106014$A7418995-ED87-4040-BBC0-FB4730F61402","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa1cb60ece5110ca2cbf85dd285906ab9594e64b","datavalue":{"value":"0649.68016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$7C5BFD67-AD90-4E40-8E34-253D10FBC503","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ea1cfd1f23a9ac9a321bcb0bb9f265ca2bb2d8cd","datavalue":{"value":"10.1007/BF02737106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$AACE2FBD-C20A-4385-97C5-0D55DCC64EBE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ebf6db346f13e0955bba67df6e3648705294a364","datavalue":{"value":{"entity-type":"item","numeric-id":1106012,"id":"Q1106012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$4D9E6AF3-068C-499A-9426-C27637280B9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"97ed3b0664441e8d880d927898de01db2ab18f95","datavalue":{"value":{"entity-type":"item","numeric-id":796291,"id":"Q796291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$58A09DA4-276A-4637-AA00-4856FAF79EAF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$4AD4421A-05CA-4940-B067-035041B92C16","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1106014$93AF8C0F-1D22-4045-B575-16ED1DA8B15C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8b14ca97823bec2dacc61a414fbea95e1f0f9fbe","datavalue":{"value":"The paper describes and illustrates a proof technique for partial correctness assertions for the programming language Distributed processes as designed by Brinch Hansen.    The specific properties of the system are 1) compositionality: proofs of programs are composed from proofs of its parts, and 2) characterization by external behavior only: the specification of some part involves actions visible on the external interface of that part only; there are no assumption commitment pairs like in the Misra \\&\\( Chandy\\) proposal [\\textit{J. Misra} and \\textit{K. M. Chandy}, IEEE Trans. Software Eng. SE-7, 417-426 (1981; Zbl 0468.68030)] or a global cooperation test as in Gerth's work [\\textit{R. Gerth}, \\textit{W. P. de Roever} and \\textit{M. Roncken}, Lect. Notes Comput. Sci. 137, 132-163 (1982; Zbl 0493.68019)].    The proof system makes visible the interface between a process and its internal procedures; both the process and its internal procedures are described using invariants where the invariants of the local procedures can invoke the values of the local variables in the process (they are external as seen from these procedures).    Although it is stated in the conclusion that the system is sound and complete no proofs for these crucial results are to be found in the paper. The reader is referred to a ph. d. thesis and an unpublished report by the authors. One has to satisfy itself with an exemplary proof of a well known sorting procedure which uses a pipeline of processors.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$FFC020D4-5145-4DEB-9DAA-94C3048BEEEF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$3B7F1B1B-B878-4F48-B427-F9A0654C121F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$4C5AF695-6F54-4608-94EC-E51DE96CE3AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$719CFFD3-3D3B-4326-9287-6EC8F4D6BB18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$E372A1F1-282B-4CCF-9FAB-4CAE5AA6CED5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d97ce25a9ed295325338e27b6315393c09c52fad","datavalue":{"value":"4060689","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$0AFF7845-77C5-4281-A536-59C772FE2534","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24c0946ca1c7cece261e7cb3d3e9af5ea3b79649","datavalue":{"value":"partial correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$1F7C6065-6444-42A7-95F1-DBD3B451CE1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15524b9b0fb4d260a9ce11193c3bc4ad3a9f642b","datavalue":{"value":"programming language Distributed processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$77658CA7-E57C-41C1-9681-D8E69EF9089B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6dfba264ed923dd13e3004a251bcdab07ddaa86e","datavalue":{"value":"compositionality","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$86EEE42A-FCB3-4CD0-B393-F0EB8CA23CD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14fca24df52ebb1d1cb643bd3c3940bc3a93324e","datavalue":{"value":"proofs of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$09C7228A-8F5F-492C-9C0C-94DEABFB9497","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e51abbec7777481743a1221a55f9c9824db8100f","datavalue":{"value":"external behavior","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106014$0A265872-EF6A-4EA0-B019-609AB210EDEF","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ca9cd2a9131e1d8839142cee57f1e863d7371382","datavalue":{"value":{"entity-type":"item","numeric-id":582045,"id":"Q582045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$CD2B780F-6A25-4B0D-90D3-E7C35D7F5AA9","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$1EAAD0FE-5FFE-4F4C-9B5D-1AB6C5625166","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ec3996c14b206674e33c3ff3678191b3d324529","datavalue":{"value":{"entity-type":"item","numeric-id":3922144,"id":"Q3922144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$91DA449B-97D9-495D-A7A2-97204C24CEE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff210c6984e92544ff3aa3044058d7dbda77eb7a","datavalue":{"value":{"entity-type":"item","numeric-id":4174727,"id":"Q4174727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$7451A709-EB48-4A40-B555-FFFD5E1BB435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$5BEEB994-05F3-44EC-B7B6-11F3502A0D47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe492de450e0ff6ffa974b52a284bea40a761f36","datavalue":{"value":{"entity-type":"item","numeric-id":3956375,"id":"Q3956375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$DAB28A4A-541F-46B2-8D7B-63F3E1F7C084","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$F7B518FD-9CF6-4135-A453-87239F5D7583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b68d01684c688b76f9852f57744d277bca068de","datavalue":{"value":{"entity-type":"item","numeric-id":3321433,"id":"Q3321433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$755BC1A8-6D93-4E95-949C-640E9EE81A62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0817097b6d61530cc9a7e9ec3f78c24eda4ab674","datavalue":{"value":{"entity-type":"item","numeric-id":1153686,"id":"Q1153686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$1D92A6D8-18FF-4D91-AD55-5A64A94A70B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a98806b17c2bbcd29d4513072d41db9b6317d23","datavalue":{"value":{"entity-type":"item","numeric-id":3681905,"id":"Q3681905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106014$544DDB9D-5B59-4C9E-B766-0E80CEB0075F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5d3ad71aad95b164c9370e0683b1272a41727395","datavalue":{"value":"https://doi.org/10.1007/bf02737106","type":"string"},"datatype":"url"},"type":"statement","id":"Q1106014$07618900-FA2E-4116-80DB-89E751E89750","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"71b634284be2f1120b5fd7b00479340b45827b64","datavalue":{"value":"W4250818063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106014$7F225A27-2057-4622-9D61-C38FFDDF9C7F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"344c9f9e26dabad61dc24359e63238d6f7ec89f2","datavalue":{"value":{"entity-type":"item","numeric-id":3678655,"id":"Q3678655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95742a1949c36c5ec576a8a3bdd058913a4d027a","datavalue":{"value":{"amount":"+0.8919691","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$D21AE88F-4748-4B56-944A-14B727EB4BC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a54033ca11b10d6cbc68a1024d7df16b9217d30","datavalue":{"value":{"entity-type":"item","numeric-id":3731019,"id":"Q3731019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4faa21490369d3b6221d9e13738d637db987c6c0","datavalue":{"value":{"amount":"+0.8829274","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$266F758D-E93A-4CD8-91ED-F7E4AC704ED6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e894f4370640765fe8d2d72578b227be58d633d","datavalue":{"value":{"entity-type":"item","numeric-id":1285659,"id":"Q1285659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"314bf9f17618e575e6432416dd3848657e6c464b","datavalue":{"value":{"amount":"+0.86027384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$C4EE2CA1-FE7D-43DE-AFBB-A6E4AC78BAC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ba2de0735a98e19f269809981a88c74ef2b07ed","datavalue":{"value":{"entity-type":"item","numeric-id":3350772,"id":"Q3350772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be2a0d0bf62ec1f015c7975b5bb49301aadf64a4","datavalue":{"value":{"amount":"+0.8577927","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$37085A90-AF65-4A56-9548-F4795EBC1714","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"def72f32b54cd209d9c8d1e27983a6d9a6a88914","datavalue":{"value":{"entity-type":"item","numeric-id":3678654,"id":"Q3678654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27306089f2719e2eec3b75bebc1e9f1196b1cfa5","datavalue":{"value":{"amount":"+0.85724425","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$BBD1408A-8836-4F92-A9EF-75B6A26EE457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4657f223a476d3721ee27cccbd9cb0e5c9544240","datavalue":{"value":{"entity-type":"item","numeric-id":1200917,"id":"Q1200917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10f49dfc4b49cc4c46e30e50d337a6890bc2f9ec","datavalue":{"value":{"amount":"+0.8516334","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$E0F4813A-0725-4A3F-878D-948AE1E04C98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d3ba2e6e5e1361ace684e95aec0deebe8844a28","datavalue":{"value":{"entity-type":"item","numeric-id":1059388,"id":"Q1059388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0db29c6c288e88a772faae5767ff459858ad1ab0","datavalue":{"value":{"amount":"+0.84775454","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$47DF2CB7-E12E-4B69-8F2D-319A126EC86F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53dbad58ef6d966cd250e986cd4236bc15c2be53","datavalue":{"value":{"entity-type":"item","numeric-id":678251,"id":"Q678251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ecc7eee925fce96a3ffd3f563aaaaba65741e54","datavalue":{"value":{"amount":"+0.842246","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$0E6BCB93-3632-45CB-817A-FF91EFDB2C0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7d7045f2d31c534448bdcd51e9fe2bbe8f64104","datavalue":{"value":{"entity-type":"item","numeric-id":757079,"id":"Q757079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b1c848effc1a3400c90fa4b01908ac7893e4695","datavalue":{"value":{"amount":"+0.8288923","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1106014$282CDE7A-349E-4E93-9AEF-D114345C1B46","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A proof system for distributed processes","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_proof_system_for_distributed_processes"}}}}}