Описание тега hoare-logic

Описание тега Вопросы с тегом

NoneHoare-logic - это формальная система для демонстрации правильности программ

1 ответ

Код разделения Hoare, используемый в Quicksort (ссылка на книгу Кормена), переходит в бесконечный цикл

Я кодирую Quicksort, используя разделение Hoare из книги Cormen Algorithms. Я не могу обнаружить никаких ошибок в своем коде, и он выглядит так же, как псевдокод в книге. swapping i, j : 0, 8 -2 2 -5 -3 6 0 1 0 -1 4 swapping i, j : 1, 3 -2 -3 -5 2 6…

26 апр '17 в 04:40

1 ответ

Тройка Hoare с неизвестной переменной в постусловии

Я рассуждаю об упражнении Hoare Logic. Я должен найти все логические выражения B и все программы S а также P которые удовлетворяют тройной {true} if B then S; if B then P; {a >= 0}, предполагая, что оценка B не может изменить магазин, но выполнен…

correctness hoare-logic

17 сен '13 в 10:43

1 ответ

Предоставляет ли Python поддержку Предположений в качестве предварительных условий?

Допущения в модульных тестах Python Предоставляет ли Python поддержку Предположений, которые будут использоваться в качестве предварительных условий для тестов, аналогичных тем, которые предоставляются JUnit с assumeThat(...) методы для Java. Это ва…

python python-3.x unit-testing hoare-logic

06 дек '18 в 16:03

2 ответа

Объяснение алгоритма разбиения Hoare

Согласно псевдокоду, приведенному на многих сайтах, я написал это Hoare алгоритм секционирования, который принимает массив, начальный и конечный индексы подмассива, подлежащего разделению, на основе заданной оси. Он работает нормально, но может кто-…

python partitioning hoare-logic

22 сен '12 в 15:02

1 ответ

Алгоритм Hoare Quicksort не работает должным образом

Так с массивом [6, 3, 8, 7, 2, 5, -9, 1, 4, 10] используя алгоритм разбиения Хоара я ожидаю [-9, 1, 2, 3, 4, 5, 6, 7, 8, 10] Но алгоритм из моего кода дает мне [4, 3, 8, 7, 2, 5, -9, 1, 6, 10] я слежу за этим алгоритмом дословно в основном algorithm…

javascript sorting hoare-logic

04 фев '19 в 04:58

0 ответов

Цикл-инвариантная логика Hoare

Каким будет цикл-инвариант для цикла ниже? {x<7} while (y < n) { y := y + 1; x := x + 1; if (x = 7) then x := 0 else x := x } {x<7} И какой будет вариант для этого же цикла?

hoare-logic

07 окт '18 в 13:39

3 ответа

Является ли {true} x:= y { x = y } действительной тройкой Хоара?

Я не уверен что { true } x := y { x = y } является действительной тройкой Хоара. Я не уверен, что один может ссылаться на переменную (в этом случае, y), без явного определения его сначала либо в теле тройной программы, либо в предварительном условии…

logic hoare-logic

02 окт '11 в 20:14

1 ответ

Нахождение инварианта цикла - Тройка Хоара

Из следующего кода мне нужно вывести / выбрать инвариант цикла. (|true|) x = 0 ; s = 0 ; while ( x <= n ) { s = s + x ; x = x + 1 ; } (|s = n(n + 1)/2|) Решение дано было s = (x-1)*x/2 ∧ (x ≤ n +1) Я не совсем понимаю, как он достиг решения выше.…

while-loop logic loop-invariant predicates hoare-logic

15 апр '18 в 16:13

1 ответ

Что такое инвариант цикла данной программы?

Я не знаю, как найти инвариант цикла. Я не уверен, с чего начать. Может кто-нибудь найти инвариант цикла данной программы и объяснить ваш метод, пожалуйста. {n ≥ 0 ∧ i = 0} while i < n − 1 loop b[i] := a[i + 1]; i:=i + 1 end loop {∀j.(0 ≤ j < …

loops proof loop-invariant hoare-logic

20 мар '18 в 04:31

1 ответ

Доказательство правильности в формальной логике

Мне было интересно, если кто-нибудь может помочь мне ответить на этот вопрос. Это из предыдущей экзаменационной работы, и я смог узнать ответ, готовый к экзамену этого года. Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно …

proof formal-methods proof-of-correctness post-conditions hoare-logic

24 май '12 в 21:37

0 ответов

Использование правила следствия

У меня есть следующий пример, который я должен доказать {a>7 ^ b>=0} n=a-b {n<a ^ a+b>=0} Используя правило следствия, я предположил, что P истинно {true} n=a-b {n<a ^ a+b>=0} логично, что Q должен быть правдой, но я не уверен, что…

proof hoare-logic

19 ноя '17 в 21:03

1 ответ

Логика Хоара

Дайте доказательство правильности следующего. {n != 0} if n<0 then n= -n {n>0} Следующее правило вывода должно помочь {B and P} S {Q}, (not B) and P=>Q --------------------------------- {P}if B then S{Q} Я искал во всем Интернете четкое объ…

proof language-concepts hoare-logic

01 окт '14 в 08:52

2 ответа

Доказательство правильности алгоритма

proof formal-methods proof-of-correctness post-conditions hoare-logic

27 апр '14 в 11:23

1 ответ

Hoare Logic | Какое постусловие действительно, когда существует бесконечный цикл?

Мой учитель сказал мне, что верно следующее утверждение: {x > 3}, хотя true (x:= 3) {x = 3} Почему это утверждение верно? Это потому, что постусловие никогда не проверяется, или пост-условие теперь считается инвариантной проверкой? Короче говоря, мо…

infinite-loop post-conditions hoare-logic

03 ноя '18 в 17:07

1 ответ

Hoare Logic, рассчитать предварительное условие

if x < 15: x = x+1 else: x = 0 почтовое условие: Q = {0 <= x <= 15} является правильным предварительным условием P1 = {-1 <= x} или P2 = {0 <= x <= 15} И как я могу рассчитать это?

condition preconditions hoare-logic

02 авг '17 в 14:35

1 ответ

Можем ли мы разработать правила вывода логики разделения в Z3 и использовать ее для автоматической проверки некоторых реквизитов?

Можем ли мы разработать правила вывода и аксиомы о логике разделения в z3 и использовать ее для автоматической проверки некоторых реквизитов? Например," x=y /\ (x |-> z) |- x=y /\ (y |-> z)"

coq z3 hoare-logic

15 май '14 в 13:51

4 ответа

Разделение Hoare попадает в бесконечный цикл

Я пытаюсь написать функцию разбиения Hoare, которая принимает массив в качестве входных данных и разделяет его с первым элементом как pivot (я знаю, что это не очень хорошая идея, я должен использовать случайные pivots, как median-of-medians подход)…

python quicksort partitioning hoare-logic

20 сен '12 в 20:37

2 ответа

Правильность перегородки Hoare

Разделение Hoare, как указано в cormen: Hoare-Partition(A, p, r) x = A[p] i = p - 1 j = r + 1 while true repeat j = j - 1 until A[j] <= x repeat i = i + 1 until A[i] >= x if i < j swap( A[i], A[j] ) else return j при использовании этого в б…

algorithm sorting data-structures quicksort hoare-logic

03 мар '15 в 19:12

0 ответов

Инвариант петли и вариант для петли

Каким должен быть цикл, инвариантный, а также вариант для данного цикла с точки зрения логики Хоара? {Правда} x := 0; y := 0; while (x < a) x := x + 2; y := y + 1; {x = 2 ∗ y} I thought of variant as (a-x)/2 and loop invariant as (x=2*y & x&l…

hoare-logic

07 окт '18 в 10:11

1 ответ

Раздел Hoare не работает, когда более чем одно значение равно pivot

Я пытаюсь написать свою собственную функцию разбиения Hoare, чтобы лучше понять это. Я думал, что хорошо следовал его определению и псевдокоду, но, несмотря на то, что во многих случаях он работает, как и ожидалось, он разваливается и входит в беско…

python algorithm sorting quicksort hoare-logic

09 июл '16 в 23:30