Applying Program Transformations for Deductive Verification of the List Reverse Program

2021 ◽  
Vol 12 (3) ◽  
pp. 127-139
Author(s):  
V. I. Shelekhov ◽  
Keyword(s):  
Program Transformations ◽  
Data Types ◽  
Deductive Verification ◽  
C Language ◽  
Recursive Program ◽  
Smt Solvers ◽  
Source Program ◽  
Predicate Language ◽  
Transformation Methods ◽  
Recursive Data

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

Design and Implementation of High-Level Numerical Analysis Functions Based on Computational Arrays for Applications in Engineering

2000 ◽  
Author(s):  
Harry H. Cheng ◽  
Xudong Hu ◽  
Bin Lin
Keyword(s):  
Numerical Analysis ◽  
Variable Number ◽  
Data Types ◽  
Real Numbers ◽  
Mathematical Functions ◽  
C Language ◽  
Complex Arithmetic ◽  
Design And Implementation ◽  
Complex Functions ◽  
High Level

Abstract This paper presents the design and implementation of high-level numerical analysis functions in CH, a superset of C language developed for the convenience of scientific and engineering computations. In CH, complex number is treated as a built-in data type, so that the syntaxes of complex arithmetic, relational operations, and built-in mathematical functions are the same as those for real numbers. The variable number of arguments is used in the built-in mathematical functions to simplify the computation of different branches of multi-valued complex functions. The computational arrays are introduced to handle the arrays in the numerical computations. Passing arrays of variable length by arrays of deferred-shape and arrays of assumed-shape to functions are discussed. These methods allow the arrays to be passed with their rank, dimensions and data types. A list of high-level numerical functions and two examples of the applications in the scientific and engineering are given in the paper.

scholarly journals A Brief Introduction to the PVS2C Code Generator

10.29007/v7k2 ◽  
2018 ◽  
Author(s):  
Natarajan Shankar
Keyword(s):  
Higher Order ◽  
Specification Language ◽  
Functional Language ◽  
Data Types ◽  
Code Generator ◽  
Numeric Data ◽  
Recursive Data

We present a brief tutorial on the PVS2C code generator for producing C code from an applicative fragment of the PVS specification language. This fragment roughly corresponds to a self-contained functional language. The tutorial covers the generation of C code for numeric data types and associated operations, arrays, recursive data types, and higher- order operations.

Partially strict non-recursive data types

1993 ◽  
Vol 3 (2) ◽  
pp. 191-215 ◽  
Author(s):  
Eric Nöcker ◽  
Sjaak Smetsers
Keyword(s):  
Data Type ◽  
Functional Languages ◽  
Data Types ◽  
Composite Object ◽  
Space And Time ◽  
Input And Output ◽  
The Individual ◽  
Recursive Data

AbstractValues belonging to lazy data types have the advantage that sub-components can be accessed without evaluating the values as a whole: unneeded components remain unevaluated. A disadvantage is that often a large amount of space and time is required to handle lazy data types properly. Many special constructor cells are needed to ‘glue’ the individual parts of a composite object together and to store it in the heap. We present a way of representing data in functional languages which makes these special constructor cells superfluous. In some cases, no heap at all is needed to store this data. To make this possible, we introduce a new kind of data type: (partially) strict non-recursive data types. The main advantage of these types is that an efficient call-by-value mechanism can be used to pass arguments. A restrictive subclass of (partially) strict non-recursive data types, partially strict tuples, is treated more comprehensively. We also give examples of important classes of applications. In particular, we show how partially strict tuples can be used to define very efficient input and output primitives. Measurements of applications written in Concurrent Clean which exploit partially strict tuples have shown that speedups of 2 to 3 times are reasonable. Moreover, much less heap space is required when partially strict tuples are used.

On the Power of Model Theory in Specifying Abstract Data Types and in Capturing Their Recursiveness

1983 ◽  
Vol 6 (2) ◽  
pp. 127-170
Author(s):  
Alberto Bertoni ◽  
Giancarlo Mauri ◽  
Pierangelo Miglioli
Keyword(s):  
Model Theory ◽  
Point Of View ◽  
Necessary Condition ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Definition Of ◽  
Recursive Data ◽  
Better Than

In this paper a comparative analysis of some algebraic and model-theoretic tools to specify abstract data types is presented: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze various notions such as “initiality”, “finality”, “monoinitiality”, “epifinality”, “weak monoinitiality” and “weak epifinality”, both from the point of view of “abstractness” and of “cardinality”, in a general model theoretical frame. For the second aspect, it is shown that only “initiality”, “monoinitiality”, “epifinality” and “weak epifinality” allow us to select countable models (for theories with a countable language), a necessary condition to get recursive data types, while this is not the case for “finality” and “weak monoinitiality”. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the “abstractness” requirement. We also show that none of the above quoted categorial notions captures recursiveness. Finally, we consider our own definition of “abstract data type”, based on typically model-theoretic notions, and illustrate the sense according to which it captures recursiveness.

Sign in / Sign up

Export Citation Format

Share Document