• Гідрологія і Гідрометрія
• Господарське право
• Економіка будівництва
• Економіка природокористування
• Економічна теорія
• Земельне право
• Історія України
• Кримінально виконавче право
• Медична радіологія
• Методи аналізу
• Міжнародне приватне право
• Міжнародний маркетинг
• Основи екології
• Предмет Політологія
• Соціальне страхування
• Технічні засоби організації дорожнього руху
• Товарознавство продовольчих товарів

Аксіоматика простих типів даних

Прості типи – це перелічувані типи, а також “цілий – integer (i)”, “дійсний – real (r)“, “булевий – boolean (b)“ і “символьний – character (с)“. Вони мають вигляд:

type T = X (х₁, х₂, .... х_n),

де Т – ім'я типу, а ( х₁, х₂, ...., х_п ) – імена значень з множини значень X типу Т.

Операції над перелічуваними типами включають бінарні операції співставлення й унарні операції pred і succ, що задають відповідно попередній та наступний елементи в множині X. Операції співставлення (<, ≤, >, ≥, = , ≠), далі (≤), визначають лінійний порядок елементів множини X.

Булевий тип визначений на множині значень Х^b і операцій Ω^b:

Х^b = {false, true},

Ω^b = {&, V, , pred, succ, ≤}.

Символьний тип визначений на множині значень Х^с і множині операцій Ω^c :

Х^с = {... , ’А’ ... , ’Х ’ ... , ’0’, ’1’, . .. , ’9’},

Ω^c ={pred, succ, ord, chаr, ≤}.

Операція ord додає кожному символові його порядковий номер, а chаr для цього номера – значення.

Аксіоми даних типів мають такий вид:

X . min X, X . max X,

( x X) & ( x ≠ X . max) succ (x) X.

( x X)& ( x ≠ X . max) succ (x)≠ X . min,

де X.min і X.max – мінімальний та максимальний елементи множини X.

Числові типи (integer і real) мають обмеження, зв'язані з архітектурою або з явним описом параметрів компонентів. Їм відповідають базові типи, обумовлені як відрізки виду:

type T = (X.min, …, X.max),

де X.min і X.max мінімальний та максимальний елементи цього відрізку. Для будь-якого х Х виконується умова х.min < х < х.max. Значення х залежить від реалізації цього типу конкретним транслятором з урахуванням архітектури комп'ютера.

Над змінними цілого типу виконуються аналогічні операції, до них додаються операції цілочисельної арифметики: унарні мінус, +, –, , div і mod Цілий тип даних на заданому відрізку визначається наступними аксіомами:

Xⁱ = {Хⁱ.min, Xⁱ.max + 1, … Хⁱ .max},

Ωⁱ = {+, , div, –, ≤},

type Tⁱ = (Xⁱ.min ,…, Xⁱ .max).

Дійсний тип визначається за допомогою операцій співставлення і звичайних арифметичних операцій (унарний мінус, +, –, , /). Аксіоми речовинного типу на відрізку такі:

Х^r = {x | Х^r.min ≤ x ≤ Х^r.max },

Ω^r = {+, , /, – , ≤ },

type T^r = (Х^r.min ,…,Х^r max).

Будь-які типи даних приводяться до базового типу, перетворюються до необхідного виду, заданого в програмі, і після одержання результату базовий тип приводиться до вихідного типу за допомогою наступних аксіом:

( x X) Т(Т⁰(х)) = х,

( x₁ X) & ( x₂ X) ( x₁ ≤ x₂ ) ≡ (T⁰(x₁) ≤. T⁰(x₂)) .

В них Т⁰позначає базовий тип для типу Т. Операції перетворення значення Т⁰(х) до Т(х) визначають відповідний базовий тип при виконанні арифметичних операцій :

( x₁ X) & ( x₂ X) (x₁ x₂) ≡ T(T⁰(x₁) T⁰(x₂)).

Читайте також:

1. I етап. Аналіз впливу типів ринку на цінову політику.
2. Автоматизований банк даних (АБД).
3. Аксіоматика структурних і складних типів даних. Структурні типи даних.
4. Аналіз даних засобами Excel
5. Аналіз паралельного інтерейсу з DSP-процесорами: запис даних в ЦАП, що під’єднаний до адресного простору пам’яті
6. Аналіз паралельного інтерфейсу з DSP-процесорами: читання даних з АЦП, що під’єднаний до адресного простору пам’яті
7. Аналіз статистичних даних про склад та плинність кадрів, які обіймали керівні
8. Аналіз та інтерпретація одержаних даних
9. Архіватори даних.
10. Архітектура баз даних
11. Аудит розрахунків за відшкодуванням завданих збитків

Переглядів: 891