loop-invariant

2熱度

1回答

有關終止函數定義的問題。我們有一個相對簡單的函數來計算輸入的₂log2n⌋。 LOG2 Configuration: {[r, n] | Integers r ≥ 0 and n ≥ 1} [r, n] -> [r + 1, n/2] if n > 1 ∧ n even [r, n] -> [r, n − 1] if n > 1 ∧ n odd 而且我們問過一些終端功能μ（R，N）是否

-2熱度

2回答

循環不變，沒有返回值，有可能嗎？和程序的正確性

所以我正在寫這個程序，它將用戶輸入存儲在鏈接列表中並將其反轉，但我有點失落。是否有可能找到不返回任何值的循環類型的循環不變量？例如一個位於main內部的循環。下面是一個循環的示例，我用它來獲取main中的用戶輸入並將其存儲在一個鏈表中，當然還有更多的代碼，但我只展示了什麼是相關的。 typedef struct node { char x; // data struct node* next

0熱度

1回答

Dafny使用交換驗證插入排序

我正在研究如何使用dafny驗證使用「交換」相鄰元素的插入排序，但我無法找到while循環的合理不變量，誰能幫我修復它？這裏是鏈接：http://rise4fun.com/Dafny/wmYME

0熱度

1回答

，在算法

k :=0 for i ←1 to n c←a[i] k←k+1 這並沒有改變的事情是要知道元素

0熱度

1回答

這是這個循環的正確不變嗎？

這對於在陣列中的線性搜索僞代碼，如果在陣列A所需元素e被發現返回一個索引i，NIL否則（這是來自CLRS書，第3版，運動2.1-3）： LINEAR_SEARCH (A, e) for i = 1 to A.length if A[i] == e return i return NIL 我試圖從中推斷循環不變的，所以根據我的理解，我認爲，一個是由事

3熱度

1回答

（Dafny）添加一個數組中的元素到另一個 - 循環不變

我有一個函數sum採用兩個陣列a和b作爲輸入並修改b使得b[i] = a[0] + a[1] + ... + a[i]。我寫了這個函數，想用Dafny來驗證它。但是，Dafny告訴我，我的循環不變可能不會被循環維護。這裏是代碼： function sumTo(a:array<int>, n:int) : int requires a != null; requires 0 <=

2熱度

1回答

我們如何定義一個循環不變式？

我們知道循環變體被定義爲在循環的每次迭代之前和之後都是真的語句。但是這個定義太鬆了嗎？讓我們看一個具體的例子：線性搜索。輸入：索引：n個A =（A 1 ，一個，一個，...，一個Ñ）和一個值v 輸出的序列我使得v = A [1]或NIL如果v是沒有在甲這裏發現是我的僞代碼： linear_search(A, v) 1 for i ∈ {1, 2, ..., n} 2 if A[i] =

0熱度

1回答

如何找到這個小代碼體的循環不變式？

前提條件：len（list）> = 2的整數列表後置條件：返回第二小的值。如果列表中存在兩個最小值，則返回最小值。 def SecondSmallest(list): 1 smallest = min(list[0], list[1]) 2 second_smallest = max(list[0], list[1]) 3 i = 2 4 while i < len(list): 5

4熱度

2回答

如何找到循環不變

我知道循環不變是爲了證明問題的正確性，但我無法完全理解如何提出一個問題，無論問題多麼微不足道。下面是一個例子，有人能指出我應該考慮採取哪一步來提出一個步驟。我知道循環中所有正在變化的值都必須包含在我的不變量中。請指導我解決這個問題，我也必須找到後期條件。一個解釋將不僅僅是一個答案;請幫忙。 {M > 0 and N >= 0 } a = M; b = N; k = 1; while (

1熱度

2回答

ValueError異常的tensorflow while_loop形狀不變

import tensorflow as tf cluster_size = tf.constant(6) # size of the cluster m = tf.constant(6) # number of contigs (column size) n = tf.constant(3) # number of points in a single contigs (column s