{"entities":{"Q1822503":{"pageid":1833245,"ns":120,"title":"Item:Q1822503","lastrevid":69237735,"modified":"2026-04-13T05:40:33Z","type":"item","id":"Q1822503","labels":{"en":{"language":"en","value":"The automated proof of a trace transformation for a bitonic sort"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4003538"}},"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":"Q1822503$51021B05-C0E9-4C3F-9514-A687E37529AC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f337d72a408d4e2ec3b0a2175af88923b848aad6","datavalue":{"value":{"text":"The automated proof of a trace transformation for a bitonic sort","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1822503$43E22145-A258-4D69-BD62-1640CD2255AF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c457fd4516745889c05ca94520e6f7aa38d53a63","datavalue":{"value":"0618.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$A1EFA04C-D5DE-428B-B3CF-2BB59DF1EF07","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1377d2146294fda5adfed37b80b83239fb2edc31","datavalue":{"value":"10.1016/0304-3975(86)90033-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$E8058B2C-256B-40A1-A3C6-0F06A527D8A3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"aa2389fcae2a0263a434a6333544a6f6de4414c5","datavalue":{"value":{"entity-type":"item","numeric-id":582033,"id":"Q582033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$D57637F0-C9FA-463F-813E-166A50AFA839","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb70dca4df364772ba1a8a49fd3075ccc08e3e3a","datavalue":{"value":{"entity-type":"item","numeric-id":582034,"id":"Q582034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$08A6B354-4529-4904-ADDD-3CBB9B1703FF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$BFB7D66B-CD82-47B1-90EF-862CA0DB6269","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-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":"Q1822503$CA29F273-6B32-4C55-A4A5-C15F1D8CC126","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3b60193e1f8771206f8ad9bbe149c10d7230720f","datavalue":{"value":"In his third volume of The Art of Computer Programming (1973; Zbl 0302.68010), \\textit{D. E. Knuth} presents Batcher's bitonic sorting network. With concurrency, this sorting network can be executed in logarithmic time. Knuth suggests a formal argument for the correctness of the bitonic sorting algorithm (as an exercise), but addresses the question of concurrency only informally. We develop a program for the bitonic sort by (1) deriving a stepwise refinement from Knuth's informal description of the algorithm, (2) deriving from the refinement a sequential execution or 'trace' of order O(n log n) in the length n of the sequence to be sorted, and (3) transforming the sequential trace into a parallel trace of order O(log n) while preserving its semantics. We shall be informal in Steps 1 and 2 - although these steps can be formalized. But we will provide a formal treatment of Step 3 and report on the certification of this treatment in a mechanized logic. This work is a contribution to the optimization of programs (via concurrency) through transformation and the automation of program proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1822503$C7706651-904F-4E3A-A94C-4FD56084CA85","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$382FF620-DA5D-4CDF-B413-1650C144AB25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$D7737BEA-0E35-4707-AA81-331A6FBA8135","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$0FB23FD3-6D0B-4CBE-9450-D24D68F6DCD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$211FC7C0-10AF-45B0-87A2-DDB7A91DEC15","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e18cbbed8d3bcaa5898d8ab0d022c7f33b9bed18","datavalue":{"value":"4003538","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$01C01436-2736-4969-B204-B2830D9F58FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b8d89333bf57ef593e22c01b5e7604e52b81557","datavalue":{"value":"bitonic sorting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1822503$BB4582BA-0769-4E02-87CC-71561403F443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1822503$660C28C7-69E7-4F85-98AE-A696E922C1EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a49d2691740729e2dd9c1c611233c1d06693479","datavalue":{"value":"stepwise refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q1822503$F0DC2CBA-7F8D-49A1-A186-E79FE11EADB5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$A8F65033-E89B-4E08-A931-A3FE5F8DC32F","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":"Q1822503$89A26BCD-2E1A-44BF-AADB-524C2086C2CF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a4cc57f7d46c38ed1cccd7ae49dfd11965aeed56","datavalue":{"value":"https://doi.org/10.1016/0304-3975(86)90033-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q1822503$62E043D2-B994-42F4-B43A-1052711EAE2E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"62a17ae994a64392c1e611e7b16a4ecb7f39e67f","datavalue":{"value":"W2091172700","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1822503$2AB12727-A8C5-4402-9455-FCB2C367D28E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"46d41c9fe05012f3b821e621dc4cf7c3fef4fcb9","datavalue":{"value":{"entity-type":"item","numeric-id":3490989,"id":"Q3490989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$55FC555B-7A57-4F8A-9D81-D8FA1BD8DF2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"226149966044b48001c0682076573b6d91099455","datavalue":{"value":{"entity-type":"item","numeric-id":4773988,"id":"Q4773988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$671F3F0C-1A03-45B9-A1C4-878C614C2AE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"924ff67e0ddb99ec0fa6c2e268cb0f96cfabe058","datavalue":{"value":{"entity-type":"item","numeric-id":3334054,"id":"Q3334054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$0A28CE01-D640-45B7-BADF-3AC10D26983A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28430ed9b4f7a26aeb0f032922db74966365595","datavalue":{"value":{"entity-type":"item","numeric-id":1843170,"id":"Q1843170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$DABED45F-5386-4DC3-A58F-1E9D38E0D626","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff81489e80366438468bf6dfe10c7a159bc3ea8c","datavalue":{"value":{"entity-type":"item","numeric-id":4057549,"id":"Q4057549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$EA477799-A3EF-4553-A876-9B5E8893A4D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8f01332146e7cd2d5499a73fb96dae34f6b2070","datavalue":{"value":{"entity-type":"item","numeric-id":1167527,"id":"Q1167527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$DD7FD978-8AA3-48BA-B027-4C89955FA4AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79258f9e3a7464bcb9f3e40943875d0fd0290494","datavalue":{"value":{"entity-type":"item","numeric-id":1167528,"id":"Q1167528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$2FA3BA71-9BCF-46CA-85AF-CA5248BC3B89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8339968df3c7c356c571548f780a15e8f9e03e66","datavalue":{"value":{"entity-type":"item","numeric-id":1819947,"id":"Q1819947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$5D637FF1-3746-416F-9EBB-D7F527160F68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc124dacefb987c3ab55cc19a55a89314cbe8faf","datavalue":{"value":{"entity-type":"item","numeric-id":3680250,"id":"Q3680250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$4A798717-F0F9-4C1F-BD73-F7C15D99E124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"176770ae40d24d71ed8218b1b621a296026799d8","datavalue":{"value":{"entity-type":"item","numeric-id":1162352,"id":"Q1162352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1822503$943541D0-8514-4A40-9FBA-3307BBA64F05","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be12cd9d14394de5ce6139854b9541c852f0ff89","datavalue":{"value":{"entity-type":"item","numeric-id":1819947,"id":"Q1819947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbd7c3e50e1ac5fe73d8ee0c68ccf2b6ec5321f2","datavalue":{"value":{"amount":"+0.7860490679740906","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1822503$1E698E57-4611-4CC7-B2ED-C328A44C30ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bea6bbb77bdec6db4f41aa2c7897e02741584aea","datavalue":{"value":{"entity-type":"item","numeric-id":917287,"id":"Q917287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e850e1a84f8063392de20b2ba79ef851e38593d9","datavalue":{"value":{"amount":"+0.7674078941345215","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1822503$A7871FBC-1075-497D-A581-FF9D7492D773","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3d8b500308ae68b68bab00239f14239b32a251b","datavalue":{"value":{"entity-type":"item","numeric-id":1318746,"id":"Q1318746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb8f44803b607dabe85a8942c22d444270f1819d","datavalue":{"value":{"amount":"+0.7614296674728394","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1822503$86C8D2F8-E4FD-4D39-8957-47E0397972D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29a51784dec193028c5e91e65703c97f98a11c9e","datavalue":{"value":{"entity-type":"item","numeric-id":3392920,"id":"Q3392920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be8e7783683755c853b9fe9eba395b82d540d7f0","datavalue":{"value":{"amount":"+0.7572498917579651","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1822503$716A2113-1827-40B2-A9FC-21D8DE0099CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae80b38f6154088b842fc26befdcd05e350ad848","datavalue":{"value":{"entity-type":"item","numeric-id":5898174,"id":"Q5898174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e40159fc283e9c855a43e7c20e7fb6d4499a749","datavalue":{"value":{"amount":"+0.7228457927703857","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1822503$CD4B1A48-BCC9-4B01-9E81-52DAE508DF45","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The automated proof of a trace transformation for a bitonic sort","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_automated_proof_of_a_trace_transformation_for_a_bitonic_sort"}}}}}