摘要:

AbstractAutomatic verification system of programs is considered to be an important constituent in software development of the supporting environment. Detailed specifications including the invariant assertion of loops, are necessary for the program verification. Thus since it is very burdensome for humans to prepare them completely, the supporting environment is desired. Thus, we have been working on a theoretical investigation regarding the generation of invariant assertions, and furthermore, the construction of a program verification system with a synthesizer of invariant assertions. The theoretical investigation has already been reported, and this paper describes the implementation of our system and presents the results. Our system is a comprehensive program verification system which includes program input, obtaining specifications (invariant assertion generation), generating verification conditions, and proving the verification conditions. As synthesizers of invariant assertions, execution of difference equation method, tracing of program variables and path conditions by symbolic execution, and proposing invariant assertions by induction from trace information are realized. These functions are explained through executive examples and using computers, it is shown that the generation of invariant assertions and its support are possible. Also, since our system, including the proof system, is realized, it is more realistic and promising than existing program verification systems.

ISSN:0882-1666    

DOI:10.1002/scj.4690200101

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThis paper describes the support system NUCSS (Nagoya University Craniofacial Surgical‐Planning System), which supports by computer the planning of craniofacial surgery using CT image. This is a total surgery planning‐assist system which plans the craniofacial surgery made traditionally by the surgeon by cutting and pasting pieces of paper on a two‐dimensional sketch of the skull image. Instead, the system displays the three‐dimensional image using computer graphics, and the planning is made interactively on the image. The major functions of the system are as follows. Generation and display of three‐dimensional image, three‐dimensional distance measurement on the skull, planning and execution of surgery on the side view of the skull, bone removal from arbitrary direction, and prediction of face after surgery. The features of the system are that the bone of arbitrary shape can be cut and shifted, and the face after surgery can roughly be predicted. This had been impossible in the traditi

ISSN:0882-1666    

DOI:10.1002/scj.4690200102

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractAs a method of dialog with users, earlier image processing systems used a combination of linear information and words, a number or a phrase for description. However, these systems were limited in providing actual detailed descriptions of the extraction of image border and border lines.Thus a new Image Processing Expert System, IMPRESS, is proposed in this paper. This system accepts sample figure presentations which include an automatic process for selecting a figure that most closely identifies the sample figure without reading a description of the processing purpose. In addition, this system can be realized by using actual cases of construction.This paper explains the basic concept of this system and the automatic construction method of the line pattern extraction procedure. The method is then applied to the problem of major outline extraction of chest X‐ray images, and its effectiveness is show

ISSN:0882-1666    

DOI:10.1002/scj.4690200103

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThis paper introduces a Prolog‐based support system for use in developing a picture recognition program. Earlier, an image recognition program was introduced using such items as cigarette packages, tableware, etc. However, because of the disadvantages of that program, a new one was necessitated.Prolog and Lisp, languages designed for use in artificial intelligence, are more suitable for use in high‐level processing, e.g., image recognition and understanding. However, Prolog shows greater potential for use in writing routines in the recognition process. But Prolog is not very effective in handling numerical calculations involving large amounts of two‐dimensional images. As a result, Prolog systems are examined herein that have been developed using additional features that allow for implementation of other languages and databases.Here, the PROFIER (PROlog system with Fortran as Image analyzER) system is described. In this system, the knowledge and control structures are written in Prolog, and for raw data processing and image feature extraction, processes that are difficult to handle with Prolog, the system is expanded for programming in FORTRAN. The configuration and characteristics of PROFIER are described, and the performance is eval

ISSN:0882-1666    

DOI:10.1002/scj.4690200104

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThe authors have been involved for 8 years on R&D as well as improvement of the production system for videotapes with digital captions for the deaf, using Japanese word processors. A prototype was developed in July 1982, and a pattern information synthesizer VIP (video information processor)‐2000 was developed in April 1983. Captions which are almost faithful to the speech of the performer were synthesized into the scene of the program, and the results were almost satisfactory. However, a certain time was needed to synthesize the caption with the video scene, which produced a delay between the caption and the mouth movement. Sometimes, the captions were difficult to read depending on the background, since no vertical edge was provided. To solve these problems, the VIP‐4000, which is a coded information synthesizer, was developed. As a result, the time for caption synthesis is reduced drastically and the vertical edge is provided. Furthermore, coloring of the characters and inhibition rules can be applied, which helps the visual sensation. This paper describes the hardware, software, features, and performances of the VIP

ISSN:0882-1666    

DOI:10.1002/scj.4690200105

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThe research and development of a 4‐valued integrated circuit, which is compatible to a binary circuit, is now being conducted intensively, aiming at the transfer of the merits of a multivalued system to a digital system. Another merit of the multivalued circuit is that the number of wirings and the wiring length can be reduced, which is useful in reducing the delay of driving due to the interwiring capacitance. On the other hand, the noise margin is a problem in the use of the multivalued circuit. From such a viewpoint, the authors are trying to improve the noise margin, and reported on the threshold control for the multivalued multithreshold circuit. In this circuit, however, the voltage step is reduced in correspondence to the control of the noise margin. This necessitates an increase of the supply voltage. As a result, when the binary ECL device is used as the circuit element, the number of levels that can be discriminated in the integrated circuit is restricted to 3 (two thresholds). This paper aims at the realization of up to a 5‐valued 12‐threshold control circuit by the binary device. For this purpose, a new threshold detector, the fundamental circuit which is obtained as an extension of that circuit, and the complementary circuit, are employed. In the threshold‐setting circuit in the threshold detector, the control value and the voltage step can be set independently, which leads to the low‐voltage supply. By introducing the signal distributor into the threshold detector, the maximum fan‐in and fan‐out, as well as the maximum number of thresholds are improved drastically. As an application, the threshold control 4‐valued decoder was constructed experimentally, and it is shown that the noise margin is improved by 1.9

ISSN:0882-1666    

DOI:10.1002/scj.4690200106

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThis paper proposes to use a multiple‐valued (p‐valued) input, 2‐valued output logical element ((p, 2)‐logical element) for the construction of a 2‐valued ULM (Universal Logic Module). The (p, 2)‐logical element can conveniently be programmed to work as an expected 2‐valued logical function by appropriately selecting two input values amongpvalues. The (p, 2)‐logical element as a ULM also has some preferable points such that the interconnections between ULM's can be decreased in VLSI, compared with the ULM in usual

ISSN:0882-1666    

DOI:10.1002/scj.4690200107

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractThis paper proposes an encoding scheme based on the concept of vector quantization, an encoding method for storing a large amount of digital line‐drawings. The vector quantization is a well‐known concept as a highly efficient encoding method for speech and image at low transmission rate. In time‐series data such as speech, the mean‐square distortion per sample is employed as the measure for the distortion in quantization, while in the line‐drawing, it is difficult clearly to specify the correspondence to the sample points. This paper proposes a matching by dynamic programming and demonstrates its validity. From the viewpoint that the distortion in encoding depends greatly on the connections among vector patterns, an encoding method permitting the encoding delay is proposed. It is shown that the distortion‐rate performance is improved drastically. The method is applied to a geographical map, and it was verified that a satisfactory figure is reproduced by approximately 1.0 bit per

ISSN:0882-1666    

DOI:10.1002/scj.4690200108

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractConventional Photometric Stereo can obtain the surface gradients of an object when its reflectance property is known. This paper proposes a new method of accurately obtaining the surface gradients with three light source directions under the assumption that the reflectance property of the surface is unknown. Assuming that the reflectance property is uniform over the entire surface, surface gradients can be obtained by the following two steps: (1) reflectance property parameters and the gradients of the suitable surface elements that characterize the reflectance property by solving the nonlinear simultaneous equations for them, so that a pseudo‐reflectance map is obtained; and (2) the gradient of each surface element is determined by using parameters obtained by (1). The reliability for the values of the reflectance property parameters (i. e., those for the pseudo‐reflectance map) can be improved by applying the method of selecting the surface elements that are sensitive to the reflectance property; this is called the characterized surface elements selection method. In computer experiment with 8‐bits shading resolution using three parallel light sources, the values of the reflectance property parameters can be obtained in optimum, and the accurate surface gradients for a glossy object can be determined.A mean square error in a depth measurement becomes an order of 10−2, confirming the usefulness of the proposed

ISSN:0882-1666    

DOI:10.1002/scj.4690200109

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY

摘要:

AbstractOne of the important aspects in the design of automation system is to establish some automatic transformation method from the specification by high‐level language, which is suitable for designer to the description at the circuit level. This paper formulates the circuit design as the transformation, from the recursion equation, which is a high‐level description, to the functional network FN, which is a circuit model based on the data‐flow operation. The purpose of this paper is to clarify the transformation rules for the automatic circuit design based on the theorem‐proving techniques. First, the recursion equation is formulated as the specification language, and the circuit description language for FN is designed. The theorem‐proving system for the automatic design of the circuit can be formulated as a logic system in which the axioms are the predicate expressions for the elements, and the inference rules are the transformation rules among elements. The transformation rules from the recursion equation to the circuit representation are constructed using the concept of schema corresponding to the type of the recursion equation. Since the transformation includes heuristic aspects, some transformation techniques from the schema to the circuit description (called schema transformation) as well as the decomposition‐synthesis rules in the circuit representation, are presented. A logic system based on the obtained result is presented, indicating that a theorem‐proving system for the automatic circuit design can b

ISSN:0882-1666    

DOI:10.1002/scj.4690200110

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1989

数据来源: WILEY