Prev: Cheap wholesale 2010 World Cup jerseys by paypal and free shipping
Next: Agile Practices in Industry Survey
From: Arjan on 13 Jun 2010 12:23
Hello all,

In his book "The science of programming" David Gries writes:

"Today, there are literally hundreds of papers dealing with the
axiomatic treatment of various constructs, from the assignment command
to various forms of loops to procedure calls to coroutines. Even the
'goto' has been axiomatized, and, indeed, very simply."


Does anyone know a good example of such a paper?



Regards,
Arjan
From: Gene on 13 Jun 2010 22:21
On Jun 13, 12:23 pm, Arjan <ar...(a)example.com> wrote:
> Hello all,
>
> In his book "The science of programming" David Gries writes:
>
> "Today, there are literally hundreds of papers dealing with the
> axiomatic treatment of various constructs, from the assignment command
> to various forms of loops to procedure calls to coroutines. Even the
> 'goto' has been axiomatized, and, indeed, very simply."
>
> Does anyone know a good example of such a paper?

This is a classic:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

From: Ben Bacarisse on 14 Jun 2010 22:11
Gene <gene.ressler(a)gmail.com> writes:

> On Jun 13, 12:23 pm, Arjan <ar...(a)example.com> wrote:
>> Hello all,
>>
>> In his book "The science of programming" David Gries writes:
>>
>> "Today, there are literally hundreds of papers dealing with the
>> axiomatic treatment of various constructs, from the assignment command
>> to various forms of loops to procedure calls to coroutines. Even the
>> 'goto' has been axiomatized, and, indeed, very simply."
>>
>> Does anyone know a good example of such a paper?
>
> This is a classic:
>
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

It is indeed, but I took the OP to be asking about axiomatising goto
which that paper does not do. If the OP was asking a more general
question about axiomatic treatment of programming constructs, then he or
she should have cut off the Gries quote a sentence early.

--
Ben.
From: Gene on 14 Jun 2010 22:34
On Jun 14, 10:11 pm, Ben Bacarisse <ben.use...(a)bsb.me.uk> wrote:
> Gene <gene.ress...(a)gmail.com> writes:
> > On Jun 13, 12:23 pm, Arjan <ar...(a)example.com> wrote:
> >> Hello all,
>
> >> In his book "The science of programming" David Gries writes:
>
> >> "Today, there are literally hundreds of papers dealing with the
> >> axiomatic treatment of various constructs, from the assignment command
> >> to various forms of loops to procedure calls to coroutines. Even the
> >> 'goto' has been axiomatized, and, indeed, very simply."
>
> >> Does anyone know a good example of such a paper?
>
> > This is a classic:
>
> >http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=...
>
> It is indeed, but I took the OP to be asking about axiomatising goto
> which that paper does not do.  If the OP was asking a more general
> question about axiomatic treatment of programming constructs, then he or
> she should have cut off the Gries quote a sentence early.
>

True enough. I don't know the entire literature, but hoped someone
sharp enough to be seeking information on axiomatic semantics could
type the Hoare reference into Google Scholar or CiteSeer and follow
links to whatever he or she wants.

From: Richard Harter on 14 Jun 2010 23:06
On Sun, 13 Jun 2010 16:23:05 GMT, Arjan <arjan(a)example.com>
wrote:

>Hello all,
>
>In his book "The science of programming" David Gries writes:
>
>"Today, there are literally hundreds of papers dealing with the
>axiomatic treatment of various constructs, from the assignment command
>to various forms of loops to procedure calls to coroutines. Even the
>'goto' has been axiomatized, and, indeed, very simply."
>
>
>Does anyone know a good example of such a paper?

Knuth did a paper which references axiomatizing the 'goto'. If
you like, I can dig up the references - as I recall it was
someone else that did the dirty work. The key idea is simple
enough; establish a precondition for each transfer label. A goto
transfer is only valid if the precondition is true when the
transfer is made.


Richard Harter, cri(a)tiac.net
http://home.tiac.net/~cri, http://www.varinoma.com
Reality is real; words are real too.
However words are not reality.
 |  Next  |  Last
Pages: 1 2
Prev: Cheap wholesale 2010 World Cup jerseys by paypal and free shipping
Next: Agile Practices in Industry Survey