Редактирование: МФСП, 02 семинар (от 08 сентября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 243: | Строка 243: | ||
Явное задание: | Явное задание: | ||
- | name: Type = val #задание | + | name: Type = val #задание знач. |
Пример: x : Int = 5 | Пример: x : Int = 5 | ||
Строка 251: | Строка 251: | ||
x : Int • x > 0 | x : Int • x > 0 | ||
- | Аксиоматически: можно | + | Аксиоматически: можно исп. оба варианта |
В разделе опис. констант: x: Int | В разделе опис. констант: x: Int | ||
В разделе опис. аксиом: | В разделе опис. аксиом: | ||
Строка 259: | Строка 259: | ||
Функции в RSL: | Функции в RSL: | ||
- | * Всюду | + | * Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^ |
∀ x: T1 • !∃ y : T2 • f(x)=y | ∀ x: T1 • !∃ y : T2 • f(x)=y | ||
- | * Частично | + | * Частично выч. Для нек-рах зн. x могут иметь 0, 2 или более значений |
'''value''' | '''value''' | ||
Строка 283: | Строка 283: | ||
post r>x /* постусловие, связывающее аргументы и значения функции */ | post r>x /* постусловие, связывающее аргументы и значения функции */ | ||
- | Пример | + | Пример пис. квадратного корня: |
sqrt : Real трелочка с тильдой Real | sqrt : Real трелочка с тильдой Real | ||
sqrt(x) as s | sqrt(x) as s | ||
Строка 295: | Строка 295: | ||
∀x"Int • f(x) ≡ x | ∀x"Int • f(x) ≡ x | ||
- | Пример с sqrt: для частично вычислимой функции предусловие переносится в начало | + | Пример с sqrt: для частично вычислимой функции предусловие переносится в начало импл. |
'''value''' | '''value''' | ||
sqrt : Real трелочка с тильдой Real | sqrt : Real трелочка с тильдой Real |