#scope #global-variables #coq #local-variables #coqide
#область #глобальные переменные #coq #локальные переменные #coqide
Вопрос:
Я пытаюсь смоделировать глобальные и локальные переменные в Coq, но я даже не знаю, с чего начать. Есть ли кто-нибудь, кто может дать мне подсказку или несколько советов? Я прочитал много документации об этом языке программирования, но не могу в этом разобраться. Заранее благодарю вас!
Комментарии:
1. Вы хотите что-то доказать о программе, написанной на языке с глобальными переменными? Или вы хотите написать программу на языке Coq? (Если это последнее, какую программу вы хотите написать, и почему она должна использовать глобальные переменные?)
Ответ №1:
Это зависит от того, что вы подразумеваете под «локальным» и «глобальным». Переменные в Coq работают иначе, чем в большинстве языков программирования, потому что их нельзя изменить. Наиболее близким к глобальной переменной является определение верхнего уровня, а наиболее близким к локальной переменной будет локальное определение:
Definition i_am_a_global : nat := 42.
Definition my_function (my_parameter : nat) : nat :=
(* Function parameters are always local *)
let my_local := my_parameter my_parameter in
my_local i_am_a_global.
Комментарии:
1. Я понимаю вашу точку зрения и понимаю, что вы мне объяснили (очень признателен, кстати). Дело в том, что я пытаюсь «переписать» некоторые функции из C в Coq, и это было для меня сложной задачей, потому что я научился использовать переменные в Coq, но не создавать какой-то новый тип (область видимости), который может быть либо глобальным, либо локальным.
2. @geeky90846 Может быть, вы могли бы включить в свой вопрос фрагмент кода на C , который вы хотели бы перевести в Coq.
3. Давайте рассмотрим эту программу: // Объявление глобальной переменной: int g; int main () { // Объявление локальной переменной: int a, b; // фактическая инициализация a = 10; b = 20; g = a b; cout << g; возвращает 0; }
4. @geeky90846 Я не уверен, какую именно функцию вы хотели бы перевести. Обычно в Coq вы не можете создавать выходные данные из программы. И нет способа сначала объявить переменную и только потом ее определять…
5. Хорошо, я думаю, я понял! Спасибо, что помогли мне!