构造类型论与计算机程序设计

Recent years,in the area of computer programming language theories,automated deduction,and more generalized area of logic and computing,a lot of systems based on constructive type theory are used widely to design type system for computer programming languages,to do formal system develpment and verification,and to be used as foundation of mathematics and computing.constructive type theory provides computer scientists with a framework to combine logic and computer program design in an elegant and flexible way.In this paper,the evolvement of constructive type theory is first introduced.The several foundations of type theory are then discussed,together with analysis of the relationships between them.The relation between constructive type theory and computer programming is explored in-depth.In the last,Martin Lof‘‘‘‘s intuitionistic type theory is used as an example to demonstrate how to do program development and verification in the same formal system.     

Aspect-oriented approach to operating system development empirical study

This paper presents a case-study where a new programming technique is applied to an established branch of software development. The purpose of the study was to test whether or not aspect-oriented programming （AOP） could be used in operating systems development. Instead of any real world operating system an educational OS with the name Nachos was used. This was because Nachos is written in Java which makes it easy to introduce aspect-oriented techniques. In this paper a new file system for the Nachos OS is developed and then it is analyzed by profiling and metrics. The results show that it is possible to use AOP in OS development and that it is also beneficial to do so.     

A New Integrated System of Logic Programming and Relational Database

Based on the study of the current two methods-interpretation and compilation-for the integration of logic programming and relational database,a new precompilation-based interpretive approach is proposed.It inherits the advantages of both methods,but overcomes the drawbacks of theirs.A new integrated system based on this approach is presented,which has been implemented on Micro VAX Ⅱ and applied to practise as the kernel of the GKBMS knowledge base management system.Also discussed are the key implementation techniques,including the coupling of logic and relational database systems,the compound of logic and relational database languages,the partial evaluation and static optimization of user‘s programs,fact scheduling and version management in problem-solving.     

An Inplementation of Pure Horn Clause Logic Programming in a Reduction System

Many reduction systems have been presented for implementing functional programming languages.We propose here an extension of a reduction architecture to realize a kind of logic programming-pure Horn clause logic programming.This is an attempt to approach amalgamation of the two important programming paradigms.     

Adaptive sliding mode-like fuzzy logic control for nonlinear systems

Sliding mode-like fuzzy logic control （SMFC） algorithm for nonlinear systems is presented in this paper. Firstly dead zone parameters of sliding mode control （SMC） are selftuned by proper adaptive laws and then combined into fuzzy logic system （FLS） to compose the opportune fuzzy logic control （FLC）, which is equivalent to the predesigned SMC controller with self-tuning parameters. Robustness and invariance to the uncertainties of the closed-loop systems are improved and chattering of the SMC is eliminated. Finally simulation results of numerical examples show that the proposed control algorithm is efficient and feasible.     

The completeness and applications of the formal system B

Since the formal deductive system (?) was built up in 1997, it has played important roles in the theoretical and applied research of fuzzy logic and fuzzy reasoning. But, up to now, the completeness problem of the system (?) is still an open problem. In this paper, the properties and structure of R0 algebras are further studied, and it is shown that every tautology on the R0 interval [0,1] is also a tautology on any R0 algebra. Furthermore, based on the particular structure of (?) -Lindenbaum algebra, the completeness and strong completeness of the system (?) are proved. Some applications of the system (?) in fuzzy reasoning are also discussed, and the obtained results and examples show that the system (?) is suprior to some other important fuzzy logic systems.     

An Implementation of Pure Horn Clause Logic Programming in a Reduction System

Many reduction systems have been presented for implementing functional programming languages.We propose here an extension of a reduction architecture to realize a kind of logicprogramming——pure Horn clause logic programming.This is an attempt to approach amalgama-tion of the two important programming paradigms.     

Controllability for single-input mechanical control systems with dissipation

Within the affane connection framework of Lagrangian control systems, based on the results of Sussmann on small-time locally controllability of single-input affine nonlinear control systems, the controllability results for mechanical control systems with single-input are extended to the case of the systems with isotropic damping, where the Lagrangian is the kinetic energy associated with a Riemannian metric, A sufficient condition of negative small-time locally controllability for the system is obtained.Then,it is demonstrated that such systems are small-time locally configuration controllable if and only if the dimemion of the configuration manifold is one. Finally, two examples are given to illustrate the results. Lie bracketting of vector fields and the symmetric product show the advantages in the discussion.     

Software Engineering in the Application of Virtual Instrument-Based Dynamics Testing System for UAV

Complex dynamics testing system for UAV can be constructed based on the virtual instrument and the software is the core LabVIEW is a graphical-based programming language with a convenient user interaction and shorter development cycle than the text-based programming language. This paper uses LabVIEW as the software development platform of the dynamics testing system for UAV. The idea of software engineering is used in the design of the testing system for UAV, and then is used to improve the reliability, stability and scalability of the testing system. The experimental results show that this system is practical, convenient to operate, able to meet the needs of the engineering and teaching for UAV research and development.     

Observer-based adaptive fuzzy control for a class of nonlinear time-delay systems

An observer-based adaptive fuzzy control is presented for a class of nonlinear systems with unknown time delays. The state observer is first designed, and then the controller is designed via the adaptive fuzzy control method based on the observed states. Both the designed observer and controller are independent of time delays. Using an appropriate Lyapunov-Krasovskii functional, the uncertainty of the unknown time delay is compensated, and then the fuzzy logic system in Mamdani type is utilized to approximate the unknown nonlinear functions. Based on the Lyapunov stability theory, the constructed observer-based controller and the closed-loop system are proved to be asymptotically stable. The designed control law is independent of the time delays and has a simple form with only one adaptive parameter vector, which is to be updated on-line. Simulation results are presented to demonstrate the effectiveness of the proposed approach.     

Category-based modularisation for equational logic programming

Although modularisation is basic to modern computing, it has been little studied for logic-based programming. We treat modularisation for equational logic programming using the institution of category-based equational logic in three different ways: (1) to provide a generic satisfaction condition for equational logics; (2) to give a category-based semantics for queries and their solutions; and (3) as an abstract definition of compilation from one (equational) logic programming language to another. Regarding (2), we study soundness and completeness for equational logic programming queries and their solutions. This can be understood as ordinary soundness and completeness in a suitable “non-logical” institution. Soundness holds for all module imports, but completeness only holds for conservative module imports. Category-based equational signatures are seen as modules, and morphisms of such signatures as module imports. Regarding (3), completeness corresponds to compiler correctness. The results of this research applies to languages based on a wide class of equational logic systems, including Horn clause logic, with or without equality; all variants of order and many sorted equational logic, including working modulo a set of axioms; constraint logic programming over arbitrary user-defined data types; and any combination of the above. Most importantly, due to the abstraction level, this research gives the possibility to have semantics and to study modularisation for equational logic programming developed over non-conventional structures. Received April 15, 1994/April 12, 1995     

Semantic Determinism and Functional Logic Program Properties

In modern functional logic languages like Curry or Toy, programs are possibly non-confluent and non-terminating rewrite systems, defining possibly non-deterministic non-strict functions. Therefore, equational reasoning is not valid for deriving properties of such programs. In a previous work we showed how a mapping from CRWL –a well known logical framework for functional logic programming– into logic programming could be in principle used as logical conceptual tool for proving properties of functional logic programs. A severe problem faced in practice is that simple properties, even if they do not involve non-determinism, require difficult proofs when compared to those obtained using equational specifications and methods. In this work we improve our approach by taking into account determinism of (part of) the considered programs. This results in significant shortenings of proofs when we put in practice our methods using standard systems supporting equational reasoning like, e.g., Isabelle.     

Exception handling in the spreadsheet paradigm

Exception handling is widely regarded as a necessity in programming languages today and almost every programming language currently used for professional software development supports some form of it. However, spreadsheet systems, which may be the most widely used type of “programming language” today in terms of number of users using it to create “programs” (spreadsheets), have traditionally had only extremely limited support for exception handling. Spreadsheet system users range from end users to professional programmers and this wide range suggests that an approach to exception handling for spreadsheet systems needs to be compatible with the equational reasoning model of spreadsheet formulas, yet feature expressive power comparable to that found in other programming languages. We present an approach to exception handling for spreadsheet system users that is aimed at this goal. Some of the features of the approach are new; others are not new, but their effects on the programming language properties of spreadsheet systems have not been discussed before in the literature. We explore these properties, offer our solutions to problems that arise with these properties, and compare the functionality of the approach with that of exception handling approaches in other languages     

Completeness of Proof Systems for Equational Specifications

Contrary to popular belief, equational logic with induction is not complete for initial models of equational specifications. Indeed, under some regimes (the Clear specification language and most other algebraic specification languages) no proof system exists which is complete even with respect to ground equations. A collection of known results is presented along with some new observations.     

Semantic foundations for generalized rewrite theories

Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications.     

Maude: specification and programming in rewriting logic

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude.     

The Software Engineering Subject Area

Besides being a generalist skilled in interpersonal communication, problem-solving, computer science fundamentals, and management and economic techniques, a computer professional also needs basic training in digital logic, organization, architecture, operating systems, data structures, file and data base systems, programming languages and translator writing systems, programming systems and methodologies, and applications and theoretical considerations. This is a large order indeed, but it is the sort of graduate that our universities must turn out if they are to meet the needs of business and industry.     

How to realize LSE narrowing

Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In Ref. 3), we introduced the LSE narrowing strategy, which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for the class of arbitrary canonical systems. LSE narrowing detects redundant derivations by reducibility tests. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be tested. In this paper, we show that many of these subterms are identical. We describe how left-to-right basic occurrences can be used to identify and exclude these identical subterms. This way, we can drastically reduce the number of subterms that have to be tested. Based on these theoretical results, we develop an efficient implementation of LSE narrowing.