Формальные методы, логика и VDM вопросы прошлых экзаменационных работ

Я надеялся, что кто-то может помочь мне со следующими вопросами, ответы были бы лучше, но если вы можете указать мне правильное направление, это также будет полезно. Я учусь на последнем курсе университета, и эти вопросы взяты из предыдущего экзамена по формальным методам, и мне не помешало бы знать ответы, готовые для статьи этого года. Наш лектор не кажется лучшим и не освещал многое из этого, поэтому найти точный ответ оказалось невозможным. Google не очень помог, как и рекомендуемые книги.

1. Учитывая, что ∃x • P (x) логически эквивалентно ¬∀x • ¬P (x) и что ∀x ∈ S • P (x) означает ∀x • x ∈ S ⇒ P (x), вывести, что ∃x ∈ S • P (x) означает ∃x • x ∈ S ∧ P (x)

2 - Опишите два утверждения, которые необходимо доказать, чтобы показать, что определение:

max(i, j)
if i>j
then i
else j

является правильной реализацией спецификации:

max(i : Z, j : Z)r : Z
pre true
post (r = i ∨ r = j) ∧ i ≤ r ∧ j ≤ r

methods logic formal-languages formal-methods
person Paul Blundell    schedule 23.05.2012    source источник
comment
Знаете ли вы, что ∃ означает существует, а ∀ означает для всех? Вы также знаете, что ∈ значит в множестве?   -  person Sachin Kainth    schedule 23.05.2012
comment
∃x • P (x) эквивалентно ¬∀x • ¬P (x), потому что если существует хотя бы один x, для которого P(x) истинно, то логически не P(x) истинно не для всех x. .   -  person Sachin Kainth    schedule 23.05.2012

Ответы (2)


arrow_upward
2
arrow_downward

Первый — это просто манипулирование символами с использованием данного и двух других хорошо известных логических эквивалентностей:

(1) ∃x • P(x) is logically equivalent to ¬∀x • ¬P(x)
(2) ∀x∈S • P(x) means ∀x • x∈S ⇒ P(x)

∃x∈S • P(x)
== ¬∀x∈S • ¬P(x) (from (1))
== ¬∀x • x∈S ⇒ ¬P(x) (from (2))
== ¬∀x • ¬x∈S v ¬P(x) (from def. of ⇒)
== ¬∀x • ¬(x∈S ∧ P(x)) (from ¬A v ¬B == ¬(A ∧ B))
== ∃x • x∈S ∧ P(x) (from (1) -- the other way around)

Во-вторых, вам нужно признать, что результат max(i, j) будет вычисляться по одному из двух путей: один, когда i<j, а другой, когда i>=j (логическое отрицание i<j)

Так что вам нужно показать, что

  1. если true ∧ i<j (предварительное условие), то (r=i ∨ r=j) ∧ i≤r ∧ j≤r (последующее условие) и
  2. если true ∧ i>=j (предконд.), то (r=i ∨ r=j) ∧ i≤r ∧ j≤r (после конд.),

где r является результатом max(i, j)

person Attila    schedule 23.05.2012
comment
Это действительно отличный ответ. - person Sachin Kainth; 23.05.2012

arrow_upward
1
arrow_downward

Но раздел 2 вашего вопроса не имеет смысла, поскольку любая реализация, возвращающая либо i, либо j, верна.

Спецификация неверна.

Правильное постусловие

post (i > j => r = i) v (i <= j => r = j)
person Echancrure    schedule 01.08.2014