Adding Constraints to Automate Programming

Thread View: comp.theory

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by Philippe BAZET Wed, 27 Jan 1993 19:51

#1869

Author: Philippe BAZET
Date: Wed, 27 Jan 1993 19:51

20 lines
976 bytes

Hi net,


Let us consider a circular list. It can be defined by an ML-like data
type such as

	list 'a = nil | cons of 'a * list 'a ;

and the assertion:

	The last element for the list is the first one.

Does anyone know of programming systems in which such assertions can be
expressed formally and used at either run-time or compile-time?  I know
of Ait Kaci's LIFE which is mainly restricted to local structure
constraints.  

Thanks in advance,
Philippe Bazet.
e-mail: bazet@cri.ensmp.fr

Re: Adding Constraints to Automate Programming

#1874

Author: Bill Pugh
Date: Thu, 28 Jan 1993 22:27

20 lines
1107 bytes

In article <BAZET.93Jan27195118@chailly.ensmp.fr> bazet@chailly.ensmp.fr (Philippe BAZET) writes:
>Let us consider a circular list. It can be defined by an ML-like data
>type such as
>
>	list 'a = nil | cons of 'a * list 'a ;
>
>and the assertion:
>
>	The last element for the list is the first one.
>
>Does anyone know of programming systems in which such assertions can be
>expressed formally and used at either run-time or compile-time? 

Check out the paper "Graph Types" by Nils Klarlund and Michael Schwartzback
in the 93 POPL conference.

	Bill Pugh
	Dept. of Computer Science
	Univ. of Maryland, College Park
	pugh@cs.umd.edu

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads