Categorical Combinators form a formal system similar to Curry’s Combinatory logic. It was developed by Curien [2] inspired by the equivalence of the theories of typed λ-calculus and Cartesian Closed Categories as sh...
详细信息
A technique is described for prototyping a system directly from a specification. the technique uses the logicprogramming language Prolog and involves translating the specification into a Prolog form. this is used in ...
ISBN:
(纸本)9780818606205
A technique is described for prototyping a system directly from a specification. the technique uses the logicprogramming language Prolog and involves translating the specification into a Prolog form. this is used in conjunction with a set of functions, also written in Prolog, which provide an operational interpretation of the semantics of the specification language, and a user interface which allows the user to exercise the specification and examine its behaviour.
the history of advances in programming - the little that there is of it - is the history of successful formalisation: by inventing and studying formalism, by extracting rigorous procedures, we progressed from programm...
ISBN:
(纸本)9780818606205
the history of advances in programming - the little that there is of it - is the history of successful formalisation: by inventing and studying formalism, by extracting rigorous procedures, we progressed from programming in machine code to programming in high level languages (HLLs). Note that before HLLs were sufficiently formalised compilers used to be unreliable and expensive to use, programs could not be ported between machines, and the very use of HLLs was more or less restricted to academia. Observe also that if today a piece of software is still difficult to port it is almost invariably due to a deviation from strict *** many application domains HLLs provide an acceptable linguistic level for program (and system) specification. One does not hear horror stories about computer applications in such domains (physics, astronomy). the expert views of such domains, their descriptive theories, can be easily expressed on the linguistic level of HLL, thus becoming prescriptive theories (specifications) for computer software. If it is desired to use computers reliably in domains where this is not the case, then we must try to narrow the gap between the linguistic level on which domain-descriptive theories are formulated and the linguistic level on which programs are prescribed (specified).the programs, as ultimately run, are always formal objects. A rigorous, calculably verifiable relationship may be defined only between formal systems (scientific theories of nature are not calculably verified; they are tested by experiments!). therefore, if we want the programs to reliably satisfy their specifications, the latter must be formal objects too. Or, put it differently: from a natural domain to a formal system there cannot lead an unbroken chain consisting of calculably verified steps only. there must be an interface at which the informality of a natural domain (or its description) comes into contact withthe formality of a computer program (or its specification). S
When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is dccidabl...
详细信息
the proceedings contain 23 papers. the topics discussed include: modeling of problem domains for driving program development systems;programming primitives for database languages;paths: an abstract alternative to poin...
ISBN:
(纸本)089791029X
the proceedings contain 23 papers. the topics discussed include: modeling of problem domains for driving program development systems;programming primitives for database languages;paths: an abstract alternative to pointers;program improvement by internal specialization;paging as a 'language processing' task;position paper on optimizing compilers;making the world safe for garbage collection;carrier arrays: an idiom-preserving extension to APL;axiomatic definitions of programming languages, II;formal program testing;the temporal logic of branching time;program logic without binding is decidable;on the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem;a program development tool;program verification based on denotational semantics;incremental evaluation for attribute grammars with application to syntax-directed editors;linear cost is sometimes quadratic;a precise inter-procedural data flow algorithm;verification of attribute grammar;dependence graphs and compiler optimizations;program optimization and exception handling;and inferring types in Smalltalk.
the proceedings contain 44 papers. the special focus in this conference is on Automata, Languages and programming. the topics include: Algorithmic specifications of abstract data types;nondeterminism in abstract data ...
ISBN:
(纸本)9783540108436
the proceedings contain 44 papers. the special focus in this conference is on Automata, Languages and programming. the topics include: Algorithmic specifications of abstract data types;nondeterminism in abstract data types;a view of directions in relational database theory;a new characterization of the regular languages;langages reconnaissables et codage prefixe pur;passes, sweeps and visits;On LALR(k) testing;on size bounds for deterministic parsers;a decision procedure for the equivalence of two dpdas one of which is linear;absolute primality of polynomials is decidable in random polynomial time in the number of variables;the deducibility problem in propositional dynamic logic;finite models for deterministic propositional dynamic logic;impartiality, justice and fairness: the ethics of concurrent termination;computing a perfect strategy for n×n chess requires time exponential in n;on the complexity of simple arithmetic expressions;proving lower bounds for linear decision trees;parikh-bounded languages;generalized Parikh mappings and homomorphisms;chomsky-Schotzenberger representations for families of languages and grammatical types;algebraically specified programming systems and Hoare’s logic;Area-time optimal VLSI networks for computing integer multiplication and Discrete Dourier Transform;automatic construction of verification condition generators from hoare logics;circular expressions: Elimination of static environments;an axiomatic approach to the Korenjak - Hopcroft algorithms;on the (generalized) post correspondence problem with lists of length 2;a sparse table implementation of priority queues;comparing and putting together recursive path ordering, simplification orderings and Non-Ascending property for termination proofs of term rewriting systems;termination of linear rewriting systems;realizing an equational specification.
A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either al...
详细信息
the proceedings contain 57 papers. the special focus in this conference is on Mathematical Foundations of Computer Science. the topics include: Lcf: A way of doing proofs with a machine;axioms or algorithms;power from...
ISBN:
(纸本)9783540095262
the proceedings contain 57 papers. the special focus in this conference is on Mathematical Foundations of Computer Science. the topics include: Lcf: A way of doing proofs with a machine;axioms or algorithms;power from power series;computational complexity of string and graph ident ification;a survey of grammar and l forms-1978;a theoretical study on the time analysis of programs;completeness problems in verification of programs and program schemes;Relationships between AFDL's and cylinders;computable data types;the problem of reachability and verification of programs;program equivalence and provability;interactive L systems with almost interactionless behaviour;on the simplification of constructions in degrees of unsolvability via computational complexity;an algebraic extension of the Chomsky — hierarchy;bounds on computational complexity and approximability of initial segments of recursive sets;on the weighted path length of binary search trees for unknown access probabilities;computational complexity of approximation algorithms for combinatorial problems;a reduct-and-closure algorithm for graphs;small universal Minsky machines;parallel and two-way recognizers of directed acyclic graphs;assertion programming;fully effective solutions of recursive domain equations;a note on computational complexity of a statistical deducibility testing procedure;context free normal systems;new proofs for jump dpda's;synchronization and maximality for very pure subsemigroups of a free semigroup;on the sets of minimal indices of partial recursive functions;some remarks on Boolean sums;on the propositional algorithmic logic;Ch(k) grammars: A characterization of LL(k) languages;a uniform approach to balanced binary and multiway trees;complexity classes of formal languages: Preliminary report.
暂无评论