*J. Loeckx and H.-D. Ehrich*

- Published in print:
- 2001
- Published Online:
- November 2020
- ISBN:
- 9780198537816
- eISBN:
- 9780191916663
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/oso/9780198537816.003.0004
- Subject:
- Computer Science, Computer Architecture and Logic Design

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing ...
More

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as VDM [Woodman and Heal, 1993]; [Andrews and Ince, 1991], Raise [Raise Development Group, 1995], Z [Spivey, 1989] and B [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as Ada [Barstow, 1983] and ML [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. Formalization leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich et al., 1989; Sannella and Tarlecki, 2001].
Less

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as *VDM* [Woodman and Heal, 1993]; [Andrews and Ince, 1991], *Raise* [Raise Development Group, 1995], *Z* [Spivey, 1989] and *B* [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as *Ada* [Barstow, 1983] and *ML* [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. *Formalization* leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich *et al*., 1989; Sannella and Tarlecki, 2001].

*Vasily Bulatov and Wei Cai*

- Published in print:
- 2006
- Published Online:
- November 2020
- ISBN:
- 9780198526148
- eISBN:
- 9780191916618
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/oso/9780198526148.003.0007
- Subject:
- Computer Science, Software Engineering

Having discussed the basic concepts of atomistic simulations, we now turn to a case study that demonstrates the use of the static simulation techniques and, along the way, reveals some of the ...
More

Having discussed the basic concepts of atomistic simulations, we now turn to a case study that demonstrates the use of the static simulation techniques and, along the way, reveals some of the realistic aspects of the dislocation core structure and highlights the coupling between continuum and atomistic descriptions of dislocations. Section 3.1 explains how to use simple solutions of the continuum elasticity theory for setting up initial positions of atoms. The important issue of boundary conditions is then discussed in Section 3.2. Section 3.3 presents several practical methods for visualization of dislocations and other crystal defects in an atomistic configuration. This first case study sets the stage for a subsequent exploration of more complex aspects of dislocation behavior, which demands more advanced methods of atomistic simulations to be discussed in Chapters 4 through 7. In Section 1.2 we already considered the atomistic structure of dislocations in simple cubic crystals. In other crystals, the atomistic structure of dislocations is considerably more complicated but can be revealed through an atomistic simulation. This is the topic of this chapter. An atomistic structure is specified by the positions xi of all atoms. In a perfect crystal, xi ´s are completely determined by the crystal’s Bravais lattice, its atomic basis and its lattice constant (Section 1.1). Now assume a dislocation or some other defect is introduced, distorting the crystal structure and moving atoms to new positions x´i . A good way to describe the new structure is by specifying the displacement vector ui ≡x'i −xi for every atom i. The relationship between ui and xi can be obtained analytically if we approximate the crystal as a continuum linear elastic solid. This is certainly an approximation, but it works well as long as crystal distortions remain small. Let us define x as the position of a material point in the continuum before the dislocation is introduced and x´ as the position of the same material point after the dislocation is introduced. Here, x is a continuous variable and the displacement vector u(x)≡x´−x expressed as a function of x is the displacement field.
Less

Having discussed the basic concepts of atomistic simulations, we now turn to a case study that demonstrates the use of the static simulation techniques and, along the way, reveals some of the realistic aspects of the dislocation core structure and highlights the coupling between continuum and atomistic descriptions of dislocations. Section 3.1 explains how to use simple solutions of the continuum elasticity theory for setting up initial positions of atoms. The important issue of boundary conditions is then discussed in Section 3.2. Section 3.3 presents several practical methods for visualization of dislocations and other crystal defects in an atomistic configuration. This first case study sets the stage for a subsequent exploration of more complex aspects of dislocation behavior, which demands more advanced methods of atomistic simulations to be discussed in Chapters 4 through 7. In Section 1.2 we already considered the atomistic structure of dislocations in simple cubic crystals. In other crystals, the atomistic structure of dislocations is considerably more complicated but can be revealed through an atomistic simulation. This is the topic of this chapter. An atomistic structure is specified by the positions xi of all atoms. In a perfect crystal, xi ´s are completely determined by the crystal’s Bravais lattice, its atomic basis and its lattice constant (Section 1.1). Now assume a dislocation or some other defect is introduced, distorting the crystal structure and moving atoms to new positions x´i . A good way to describe the new structure is by specifying the displacement vector ui ≡x'i −xi for every atom i. The relationship between ui and xi can be obtained analytically if we approximate the crystal as a continuum linear elastic solid. This is certainly an approximation, but it works well as long as crystal distortions remain small. Let us define x as the position of a material point in the continuum before the dislocation is introduced and x´ as the position of the same material point after the dislocation is introduced. Here, x is a continuous variable and the displacement vector u(x)≡x´−x expressed as a function of x is the displacement field.