Abstract:In this paper, an automatic synthesis system FP/B of systolic array is presented, in which FP algebra and rewriting system are essentially used. Some concurrent functional forms are proposed, the expansion solutions of a class of linear recursive equations can be expressed by them directly. Algorithms which can be transformed into them may have efficient and regular computing structures, so parallelism and pipelinability hidden in the original algorithms are well developed. Based on the FP/B algebra we've given the formal defintion of systolic arrays and constructed a sys totolic rewriting system with properties of termitation and correctness.FP/B user programs can be automatically rewriten into equivalent optimized systolic expressions,Which can be directly mapped into VLSI architectures according to the geometric meanings of FP/B functions and concurrent functional forms.Finally,a typical instance is given to show the synthesis process.

Abstract:This paper extends the expressive power of FP by introducing stream and recursive equations on stream for the description of parallel algorithms with cyclic data dependency and states. The decidability theorem of about whether the FP program has its systolic implementation is given. This research also shows that the systoliclizing method on graph can be easily used on FP description.

Abstract:In this paper we propose an interactive approach to program synthesis: Explicit strategies are used to guide program construction. Our approach regards program synthesis as a constructive theorem proving task. By specifying proof strategies in a higher order functional meta-language, we are able to represent the programmer s advice, mathematical inductions, program transformation rules/strategies and resolution methods in a uniform manner. The implementation of strategies depends on higher order unification.Our approach can be automatized easily.

Abstract:In this paper, we show how to represent an EBNF (Extended BNF) grammar in form of a syntax graph. We then give an algorithm to translate an EBNF grammar into its syntax graph form. We proceed to present a general parsing algorithm applicable to various procedural high level language and make considerations of error recovery and the insertion of semantic routines.

Abstract:The paper proposes a new technique for executable specifications, which directly converts a specification into a program in a programming language by taking advantage of the idea of source-to_source conversion which is based on the rules defined formally and the canonical abstract syntax trees. The technique and the corresponding supporting system possess the following virtues: supporting rapid prototyping and getting the effects of rapid prototypes well.

Abstract:In this paper, the notions of scheme simplification ordering are introduced, and a new method for proving termination rewriting is given. At the same time, scheme recursive path ordering is discussed, and the upper and lower extension of rewriting rule w.r.t. scheme set are defined. By this, finally we show how to prove termination of rewriting using scheme recursive path ordering.

Abstract:Net invariants and reachability trees are used to investigate dynamic properties of Petri Nets. Both concepts have been generalized for different classes of High Level Petri Nets. In this paper we introduce the compound token and the token flow path concepts. An algorithm for computing the S-invariants of High Level Petri Nets is presented. In the algorithm, the compound token and the token flow path ideas are adopted and all S -invariants of an HLPN can be generated by a system of integer linear equations without unfolding the net.

Abstract:Model Description Language NUMDL is an important part of JSEIDSS which is an intelligent decision support system. NUMDL provides a tool for model building and model management. It s so powerful as to concisely describe concepts and formulas of model, and it has some distinguishing features. This paper describes its design and implementation.

Abstract:REP expression class and its canonical form are presented in [1]. This paper expands this class and proves that there exists canonical form for it.