Search

We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny, and their traversal via iterators. For this purpose, we devise a verification methodology that makes it possible to implement ADTs based on already existing ones, while maintaining proper encapsulation. Then, we apply this methodology to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The approach introduced in this paper allows one to progressively refine some aspects of the specification such as iterator invalidation, so that clients of the library can reason about how structural changes to a list affect existing iterators. Finally, we extend our methodology to the verification of client code (i.e., code that makes use of the implemented ADTs) and identify the boilerplate conditions common to all methods that receive and manipulate ADTs., Ministerio de Economía y Competitividad, Ministerio de Ciencia e Innovación, Comunidad de Madrid, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny, and their traversal via iterators. For this purpose, we devise a verification methodology that makes it possible to implement ADTs based on already existing ones, while maintaining proper encapsulation. Then, we apply this methodology to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The approach introduced in this paper allows one to progressively refine some aspects of the specification such as iterator invalidation, so that clients of the library can reason about how structural changes to a list affect existing iterators. Finally, we extend our methodology to the verification of client code (i.e., code that makes use of the implemented ADTs) and identify the boilerplate conditions common to all methods that receive and manipulate ADTs., Ministerio de Economía y Competitividad, Ministerio de Ciencia e Innovación, Comunidad de Madrid, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

In this paper, we present a novel and simple Yee Finite-Difference Time-Domain (FDTD) scheme to solve numerically the nonlinear second-order thermoviscous Navier–Stokes and the Continuity equations. In their original form, these equations cannot be discretized by using the Yee’s mesh, at least, easily. As it is known, the use of the Yee’s mesh is recommended because it is optimized in order to obtain higher computational performance and remains at the core of many current acoustic FDTD softwares. In order to use the Yee’s mesh, we propose to rewrite the aforementioned equations in a novel form. To achieve this, we will use the substitution corollary. This procedure is novel in the literature. Although the scheme can be extended to more than one dimension, in this paper, we will focus only on the one-dimensional solution because it can be validated with two analytical solutions to the Burgers equation: the Mendousse mono-frequency solution and the Lardner bi-frequency solution. Numerical solutions are excellently consistent with the analytical solution, which demonstrates the effectiveness of our formulation.

Mobility data describe the movement of objects in a time interval, such as vehicles, pedestrians, animals. Commonly, mobility data take the form of spatial trajectories, i.e. sequences of timestamped positions in a coordinated space. For example, GPS trajectories are a popular class of spatial trajectories collected outdoors. In this project, we consider a variety of mobility data, including indoor trajectories collected using a positioning infrastructure based on UltraWide Band (UWB). Goal of the project is to investigate on recent Moving Object database solutions for the management of UWB trajectories with focus on recent commercial databasesfor IOT data. In particular, the goal is to analyze a recent Moving Object database called MobilityDB.

In the Address Programming Language (1955), the concept of indirect addressing of higher ranks (Pointers) was introduced, which allows the arbitrary connection of the computer’s RAM cells. This connection is based on standard sequences of the cell addresses in RAM and addressing sequences, which is determined by the programmer with indirect addressing. Two types of sequences allow programmers to determine an arbitrary connection of RAM cells with the arbitrary content: data, addresses, subroutines, program labels, etc. Therefore, the formed connections of cells can relate to each other. The result of connecting cells with the arbitrary content and any structure is called tree-shaped formats. Tree-shaped formats allow programmers to combine data into complex data structures that are like abstract data types. For tree-shaped formats, the concept of “review scheme” is defined, which is like the concept of “bypassing” trees. Programmers can define multiple overview diagrams for the one tree-shaped format. Programmers can create tree-shaped formats over the connected cells to define the desired overview schemes for these connected cells. The work gives a modern interpretation of the concept of tree-shaped formats in Address Programming. Tree-shaped formats are based on “stroke-operation” (pointer dereference), which was hardware implemented in the command system of computer “Kyiv”. Group operations of modernization of computer “Kyiv” addresses accelerate the processing of tree-shaped formats and are designed as organized cycles, like those in high-level imperative programming languages. The commands of computer “Kyiv”, due to operations with indirect addressing, have more capabilities than the first high-level programming language – Plankalkül. Machine commands of the computer “Kyiv” allow direct access to the i-th element of the “list” by its serial number in the same way as such access is obtained to the i-th element of the array by its index. Given examples of singly

The power of shared data types to solve consensus in asynchronous wait-free systems is a fundamental question in distributed computing, but is largely considered only for specific data types. We consider general classes of abstract shared data types, and classify types of operations on those data types by the knowledge about past operations that processes can extract from the state of the shared object. We prove upper and lower bounds on the number of processes which can use data types in these classes to solve consensus. Our results generalize the consensus numbers known for a wide variety of specific shared data types, such as compare-and-swap, augmented queues and stacks, registers, and cyclic queues. Further, since the classification is based directly on the semantics of operations, one can use the bounds we present to determine the consensus number of a new data type from its specification. We show that, using sets of operations which can detect the first change to the shared object state, or even one at a fixed distance from the beginning of the execution, any number of processes can solve consensus. However, if instead of one of the first changes, operations can only detect one of the most recent changes, then fewer processes can solve consensus. In general, if each operation can either change shared state or read it, but not both, then the number of processes which can solve consensus is limited by the number of consecutive recent operations which can be viewed by a single operation. Allowing operations that both change and read the shared state can allow consensus algorithms with more processes, but if the operations can only see one change a fixed number of operations in the past, we upper bound the number of processes which can solve consensus with a small constant.

As part of developing the Execution Support System of Computer-Aided Prototyping System (CAPS), there is a need to translate and schedule prototypes of hard real-time systems whose specifications are defined in a hierarchical structure by using the Prototyping System Description Language (PSDL). We present a design and implementation of a PSDL expander in this thesis. The expander translates a PSDL prototype with an arbitrarily deep hierarchical structure into an equivalent two-level form that can be processed by the current implementations of the other CAPS tools. The design of the expander also provides for inheritance of timing constraints and static consistency checking., http://archive.org/details/thedesignndimple1094528098, Lieutenant JG, Turkish Navy, Approved for public release; distribution is unlimited.

The use of several levels of abstraction has proved to be very helpful in constructing and maintaining programs. Abstract data types such as sets and lists reduce programmer time by relieving him from the petty details of low-level implementations. In the past, programming systems have provided only a single general purpose implementation for an abstract type. Thus the programs produced using abstract types were often inefficient in space or time. In this paper a system for automatically choosing efficient implementations for abstract types from a library of implementations is discussed. An example program is processed in detail.

The use of several levels of abstraction has proved to be very helpful in constructing and maintaining programs. Abstract data types such as sets and lists reduce programmer time by relieving him from the petty details of low-level implementations. In the past, programming systems have provided only a single general purpose implementation for an abstract type. Thus the programs produced using abstract types were often inefficient in space or time. In this paper a system for automatically choosing efficient implementations for abstract types from a library of implementations is discussed. An example program is processed in detail.

The image of abstract data types is examined as manysorted algebraic systems. Two abstract data types are in detail examined: natural numbers and lists.

The image of abstract data types is examined as manysorted algebraic systems. The abstract data tape as stack, queues, priority queues, binary trees and set are examined in details.

The image of abstract data types is examined as manysorted algebraic systems. The abstract data tape as stack, queues, priority queues, binary trees and set are examined in details.

The image of abstract data types is examined as manysorted algebraic systems. Two abstract data types are in detail examined: natural numbers and lists.

We introduce mCRL2, a specification language that can be used to specify and analyse the behaviour of distributed systems. This language is the successor of the mCRL specification language. The mCRL2 language extends a timed basic process algebra with the possibility to define and use abstract data types. The mCRL2 data language features predefined and higher-order data types. The process algebraic part of mCRL2 allows a faithful translation of coloured Petri nets and component based systems: we have introduced multiactions and we have separated communication and parallelism.

Restructuring software to improve its design can lower software maintenance costs. One problem encountered during restructuring is formulating the new design. A meaning-preserving program restructuring tool with a star diagram manipulable visualization can help a programmer redesign a program based on abstract data types. However, the transformational support required for meaning-preserving restructuring is costly to provide. Also, programmers encounter comprehension and recall difficulties in complex restructuring tasks. Consequently, transformations were replaced with visual and organizational aids that help a programmer to plan and carry out a complex restructuring. For example, a star diagram manipulation called trimming was added, which mimics the way that basic restructuring transformations affect the star diagram display, allowing a programmer to plan a restructuring without depending upon restructuring transformations. With the ability to annotate trimmed star diagram components, plans can be recorded and later recalled. Programmer-controlled elision was added to help remove clutter from star diagram views. We implemented a star diagram planning tool for C programs, measured its elision capabilities, and performed a programmer study. We found that elision is effective in controlling star diagram size, and the study revealed that each programming team successfully planned its restructuring in rather different, unanticipated ways. These experiments resulted in important improvements in the tool's software design and user interface.

Restructuring software to improve its design can lower software maintenance costs. One problem encountered during restructuring is formulating the new design. A meaning-preserving program restructuring tool with a star diagram manipulable visualization can help a programmer redesign a program based on abstract data types. However, the transformational support required for meaning-preserving restructuring is costly to provide. Also, programmers encounter comprehension and recall difficulties in complex restructuring tasks. Consequently, transformations were replaced with visual and organizational aids that help a programmer to plan and carry out a complex restructuring. For example, a star diagram manipulation called trimming was added, which mimics the way that basic restructuring transformations affect the star diagram display, allowing a programmer to plan a restructuring without depending upon restructuring transformations. With the ability to annotate trimmed star diagram components, plans can be recorded and later recalled. Programmer-controlled elision was added to help remove clutter from star diagram views. We implemented a star diagram planning tool for C programs, measured its elision capabilities, and performed a programmer study. We found that elision is effective in controlling star diagram size, and the study revealed that each programming team successfully planned its restructuring in rather different, unanticipated ways. These experiments resulted in important improvements in the tool's software design and user interface.

Restructuring software to improve its design can lower software maintenance costs. One problem encountered during restructuring is formulating the new design. A meaning-preserving program restructuring tool with a star diagram manipulable visualization can help a programmer redesign a program based on abstract data types. However, the transformational support required for meaning-preserving restructuring is costly to provide. Also, programmers encounter comprehension and recall difficulties in complex restructuring tasks. Consequently, transformations were replaced with visual and organizational aids that help a programmer to plan and carry out a complex restructuring. For example, a star diagram manipulation called trimming was added, which mimics the way that basic restructuring transformations affect the star diagram display, allowing a programmer to plan a restructuring without depending upon restructuring transformations. With the ability to annotate trimmed star diagram components, plans can be recorded and later recalled. Programmer-controlled elision was added to help remove clutter from star diagram views. We implemented a star diagram planning tool for C programs, measured its elision capabilities, and performed a programmer study. We found that elision is effective in controlling star diagram size, and the study revealed that each programming team successfully planned its restructuring in rather different, unanticipated ways. These experiments resulted in important improvements in the tool's software design and user interface.

Design patterns are useful for the design of object oriented systems. The power of design patterns stems from their ability to provide generic solutions to reappearing problems that can be specialized for particular situations. The implementation of design patterns however, has received little attention. We identify four problems associated with their implementation using conventional object oriented languages. First, the traceability of a design pattern in the implementation is often insufficient; the design pattern is "lost". Second, because several patterns require an object to forward messages to other objects to increase flexibility, the self problem often occurs. Third, because the pattern implementation is mixed with the domain class, the reusability of pattern implementations is often limited. Finally, implementing design patterns may present significant implementation overhead for the software engineer. Often, a potentially large number of simple methods must be implemented with trivial behavior. A solution to these problems is presented in the context of the layered object model (LayOM). LayOM provides language support for the explicit representation of design patterns in the programming language. LayOM is an extended object oriented language which contains several components that are not part of the normal object model, such as states, categories and layers. Layers are used to represent design patterns at the level of the programming language. Example layer types for eight design patterns are presented. Because LayOM is an extensible language, the software engineer may extend the language model with abstractions for other design patterns

In TAV4, the first author presented a paper describing an algorithm to perform run-time consistency checking of abstract data types specified using algebraic specifications. This algorithm has subsequently been incorporated into a run-time consistency checking tool for the Anna specification language for Ada, and works on a subset of all possible algebraic specifications. The algorithm implementation can be considered a test oracle for algebraic specifications that performs its activities while the formally specified program is running. This paper presents empirical results on the use of this test oracle on a real life symbol table implementation. Various issues that arise due to the use of algebraic specifications and the test oracle are discussed. 50 different errors were introduced into the symbol table implementation. On testing using the oracle, 60% of the errors were detected by the oracle, 35% of the errors caused Ada exceptions to be raised, and the remaining 5% went undetected. These results are remarkable, especially since the test input was simply one sequence of symbol table operations periormed by a typical client. The cases that went undetected contained errors that required very specific boundary conditions to be met - an indication that white box test data generation techniques may be required to detect them. Hence, a combination of white-box test data generation along with a specification based test oracle may be an extremely versatile combination in detecting errors. This paper does not address test data generation, rather it illustrates the usefulness of algebraic specification based test oracles during runtime consistency checking. Runtime consistency checking should be considered a complementary approach to unit testing using generated test data.

The goal of our research is to develop systematic understanding of the theory and practice of highly concurrent data objects. Despite impressive progress in hardware that has made multiprocessors readily available for parallel processing, there is little agreement on the relative merits of competing architectures, and it has often proved difficult to realize these machines' potential for parallelism. Our research exploits the theory of abstract data types to derive: (1) impossibility results, showing that certain kinds of concurrency simply cannot be achieved with certain primitives; (2) new techniques for specifying and reasoning about the behavior of concurrent objects; and (3) synchronization algorithms permitting new, higher degrees of concurrency. The resulting theory yields consequences for algorithm and programming language design. We view a concurrent system as a collection of sequential processes that communicate through shared objects. Each object has a type, which defines a set of possible values, and a set of primitive operations that provide the only means to create and manipulate that object. This model is general, encompassing both message passing architectures in which the shared objects are message queues and shared-memory architectures in which the shared objects are data structures in memory. Traditionally, interprocess synchronization theory has centered around the notion of mutual exclusion. We do not rely on mutual exclusion as the sole means to synchronize processes. Implementation of a concurrent object is WAIT-FREE if it guarantees that any process will complete any operation within a fixed number of steps, independent of the level of contention and execution speeds of other processes.

Like many new ideas, object oriented programming (OOP) does not yet have a universally accepted definition. Even the terminology of OOP can vary greatly from one system or language to another. This paper introduces OOP to the newcomer in a language-independent manner. The underlying theory of OOP is presented to give the reader the basics necessary to understand the nuances of the various OOP languages that are available. Several OOP languages are briefly considered, as are object-oriented database management systems, object-based programming, and object-oriented design. Various problem areas are explore in detail. This paper should also be of considerable help in making the transition from one OOP language to another.

Current Database Management Systems (DBMS) manage only alphanumeric data but not multimedia data. In order to have a DBMS that can handle both alphanumeric data and multimedia data, one can either build a new system or modify an existing system. The decision was to build such a system on top of an existing system, namely INGRES, using the abstract data type (ADT) concept. Unfortunately the INGRES system used does not support ADT. As a result the Multimedia Database Management System (MDBMS) prototype must design data structures that would allow the capture and retrieval of the information relating to the data in the database. Further, to implement the ADT concept for the multimedia data, additional tables need to be created that would hold information relating to the multimedia data. This process of dealing with the management of information, generally referred to as catalog management, in the MDBMS prototype is a major part of this thesis. The design of the data structures and their applications are explained. In addition, to be able to insert data into the database, operations for the creation of tables and the insertion of the data are needed. These operations are not simple, single SQL statement. Because of the potential presence of multimedia data, the generation of multiple statements may be required from one simple user statement. The thesis also discusses the design and implementation of these operations.

Atomic transactions are a widely accepted mechanism for coping with failures and concurrency in database systems, both distributed and centralized. Many algorithms have been proposed for concurrency control and recovery. Recent work has focused on typed objects, such as queues, directories, or counters, that provide a richer set of operations. Several algorithms have been proposed to enhance concurrency and recovery by exploiting data objects' type-specific properties. Most of these algorithms are locking schemes in which conflicts are governed by some notion of commutativity: lock modes for commuting operations do not conflict. This paper presents a new locking algorithm that permits more concurrency than existing commutativity-based protocols. In addition, the protocol permits operations to be both partial and non-deterministic, and it permits the lock mode for an operation to be determined by its results as well as its name and arguments. The protocol exploits type-specific properties of objects; necessary and sufficient constraints on lock conflicts are defined directly from a data type specification. We give a complete formal description of the protocol, encompassing both concurrency control and recovery, and prove that the protocol satisfies hybrid atomicity, a local atomicity property that combines aspects of static and dynamic atomic protocols. We also show that the protocol is optimal in the sense that no hybrid atomic locking scheme can permit more concurrency. Keywords: Distributed data processing, Locking, Time stamps, Local atomicity, Hybrid atomicity., Sponsored in part by Grants NSF-DCR85-10014, NSF-CCR87-16884 and ARPA Order-4976.

An advantage of distributed systems over centralized systems is that valuable data can be stored redundantly at multiple locations--a practica commonly called 'replication'. Replication can enhance the availability of data in the presence of failures, increasing the likelihood that the data will be accessible when needed. This thesis introduces a new method for managing replicated data. We propose new techniques to address four problems associated with replication: the representation and manipulation of replicated data, concurrency control, on-the-fly reconfiguration, and enhancing availability in the presence of partitions. Unlike many methods that support replication only for uninterpreted files, our method makes use of type-specific properties of objects (such as sets, queues, or directories) to provide more effective replication. Associated with each operation of the data type is a set of quorums, which are collections of sites whose cooperation suffices to execute the operation. Analysis of the algebraic structure of the data type is used to derive a set of constraints on quorum intersections. Any choice of quorums that satisfies these constraints yields a correct implementation, and it can be shown that no smaller set of constraints guarantees correctness. By taking advantage of type-specific properties in a general and systematic way, our method can realize a wider range of availability properties, more concurrency, more flexible reconfiguration, and better tolerance of partitions than existing replication methods. Keywords: Atomicity, Availability, Concurrency control, Partitions, Reconfiguration, and Reliability.

A rigorous framework for studying immutable data types having nondeterministic operations and operations exhibiting exceptional behavior is developed. The framework embodies the view of a data type taken in programming languages, and supports hierarchical and modular structure among data types. The central notion in this framework is the definition of a data type. An algebraic and behavioral approach for defining a data type is developed which focuses on the input-output behavior of a data type as observed through its operations. The definition of a data type abstracts from the representational structure of its values as well as from the multiple representations of the values for any representational structure. A hierarchical specification language for data types is proposed. A deductive system based on first order multi-sorted predicate calculus with identity is developed for abstract data types. A correctness criterion is proposed for an implementation coded in a programming language with respect to a specification. It is defined as a relation between the semantics of an implementation and the semantics of a specification. It does not require a correct implementation to have the maximum amount of nondeterminism specified by a specification. A methodology for proving correctness of an implementation is developed which embodies the correctness criterion.

data types are the basis of an emerging methodology of computer programming. The only existing languages supporting abstract data types directly, CLU and Simula, both require compacting garbage collection, and thus they are not suitable for many applications. This thesis presents the design of a new language incorporating abstract data types; the language requires only a run-time stack, and not garbage collection. This new language, called ASBAL(for 'A Stack Based Abstraction Language'), is based on CLU, and borrows as many features as possible directly from it. Virtually every significant feature of CLU is carried over into ASBAL in some form, and extensions are included when necessary. For example, the maximum size of objects becomes an issue and is resolved by the addition of size parameters to types. Also, a limited facility for dynamic storage allocation is incorporated in ASBAL to compensate for the removal of a garbage collected heap. This facility allows list and graph structures to be built within the framework of the stack while preventing dangling references as a 'side-effect' of compile-time type checking. (Author)

The concept of type has been used without a precise definition in discussions about programming languages for 20 years. Before the concept of user-defined data types was introduced, a definition was not necessary for discussions of specific programming languages. This report discusses a definition of type in which the concept of variable is considered primitive and types are defined as various equivalence classes of variables that may be legally and meaningfully substituted for one another in different contexts. Abstraction from the differences between two variables is then achieved by allowing the substitution of one variable in an equivalence class for another within specified contexts such as parameter substitution, assignment, and data sharing. The user of a language with an abstraction facility based on the preceding idea is free to group variables into types in ways meaningful to him but must state the conditions under which members of a group are equivalent. Several kinds of types are proposed for inclusion in such a language. Some examples are types defined by identical externally visible behavior (equivalent specification), types whose members differ according to the value of one or more parameters, and types whose members have identical representations. The preceding approach to type definition has a strong effect on the possibilities for code sharing, data sharing, and parameter passing. New or unusual compiling techniques will probably be required to exploit these possibilities. (Author)

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

The role of reference variables in producing efficient but insecure data structure spaghetti is similar to that played by GOTOs in un-Structured Programming. Secure programming language constructs are suggested to replace various identified uses of references. Efficiency of program implementation is maintained by allowing specifications of the desired representation method to be added to the abstract data structure definitions.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.

Předmětem této práce je tvorba pomůcek pro začínající programátory, které usnadní studentům absolvování předmětu BPPC. Teoretická část pojednává o programovacích jazycích C, C++ a jejich odlišnostech. Dále jsou zmiňovány kompilátory těchto jazyků, je zdůrazněno především vývojové prostředí MS Visual C++ 2005, ve kterém probíhá výuka předmětu BPPC a odlišnosti tohoto prostředí od standardů ISO. Jsou také probrány některé základní techniky programování v C++, které jsou často zmiňovány dále v práci. Druhou částí je implementace knihoven pro kontrolu správnosti programů. Knihovna check.h kontroluje práci programátora s dynamicky alokovanou pamětí a se soubory. Knihovna adtcheck.h umožňuje ověření správnosti a vykreslení topologie abstraktních datových typů implementovaných programátorem. K těmto knihovnám byla vytvořena webová prezentace s jejich dokumentací., The purpose of this thesis is implementation utilities for beginners in programming. These utilities could make passing subject BPPC easier. Theoretical part dissertates about programming languages C, C++ and about differences between them. There is also talked about compilers of these languages with accent for development environment MS Visual C++ 2005 and it’s diversities form ISO standards. This path contains also some basic chapters of programming, which are often noticed later. The second part is implementation libraries for checking programs. Library check.h checks programmer’s using of dynamic allocated memory and files. Library adtcheck.h was designed for checking and printing topology of abstract data types, which were implemented by programmer. There was designed also web pages with documentation for both libraries.