Partial correctness and Total correctness
in [Theory]
|
Prev: Subject: finding the $n$-th largest $d$-fold products
Next: A Feasible Optimal Solution to the P Versus NP Problem:
From: Srinu on 1 May 2010 04:50 Dear All, We know what is Partial correctness and Total correctness for sequential programs. What is Partial correctness in case of concurrent programming? And what is total correctness in this case? Srinivas
From: Hans H�ttel on 1 May 2010 14:29 In article <36a8707f-d12e-49d2-ab4b-e99fb61d67c2(a)g5g2000pre.googlegroups.com>, Srinu <sinu.nayak2001(a)gmail.com> wrote: > Dear All, > > We know what is Partial correctness and Total correctness for > sequential programs. > What is Partial correctness in case of concurrent programming? > And what is total correctness in this case? Why would the interpretation of Hoare triples not be the same? After all, we can interpret such triples with respect to any small-step semantics. Assume a program logic interpreted on configurations P, where F I= P means that F holds for configuration P. Let P ->> P' denote that P in some sequence of steps (in our small-step semantics) evolves to P', where P' is a terminal configuration. Then: {F} P {G} holds if F |= P and whenever P ->> P' for some P', then also G |= P' [F] P [G] holds if F |= P and there exists only terminal configurations P' s.t. P ->> P' for some P', and G |= P' Hans
From: Srinu on 3 May 2010 03:48 You are correct. I was looking for little answers something like below: In case of sequential programming, We define Partial correctness as: "If the program terminates, it is guarenteed to produce correct result." and define Total correctness as: "The program is guarenteed to terminate and it is guarenteed to produce correct result." But in concurrent programming we find two kinds of programs. 1. those which terminates. 2. those which never terminates. What are the definitions for partial correctness and total correctness for these two veriety of programs? Thanks and regards, Srinivas
From: Chris F Clark on 3 May 2010 09:43 For programs that are expected to terminate the definitions of partial and total correctness are the same. I have not seen a definition of either partial or total correctness for programs the are expected not to terminate. I have seen (but only cursorily as it isn't my area of interest) that people have developed theories and proof schemes for such programs. I would recommend Googling "co-inductive" as that is a word I remember associated with the topic. Hope this helps, -Chris ****************************************************************************** Chris Clark email: christopher.f.clark(a)compiler-resources.com Compiler Resources, Inc. Web Site: http://world.std.com/~compres 23 Bailey Rd voice: (508) 435-5016 Berlin, MA 01503 USA twitter: @intel_chris ------------------------------------------------------------------------------
From: Chris F Clark on 3 May 2010 12:02
Chris F Clark <cfc(a)shell01.TheWorld.com> writes: > For programs that are expected to terminate the definitions of partial > and total correctness are the same. Clarification, "the same as the original poster listed" (not the same as each other as my original wording might have suggested). Informally: If the program computes the correct result when it terminates, but may not terminate in all cases, it is partially correct. If the above holds and the program is guaranteed to terminate, it is totally correct. As I said, I don't know of any one who has tried to recast those terms for programs intended to be non-terminating. |