Недавно у меня появилась возможность обучать человека, который посещает вводный курс информатики на уровне колледжа.Класс по обучению программированию на Java.У этого человека было несколько вопросов об одной из программ Java в учебнике.Цель программы на Java - симулировать бросание монеты несколько раз, а затем сообщить о количестве головок и количестве хвостов.В книге был показан класс Java с закрытыми и открытыми разделами, конструктор класса, а в «main» используются фиксированные переменные и цикл for.Я думаю, что я успешно объяснил тонкости этих конструкций Java, но это заставило меня задуматься, действительно ли это лучший способ представить информатику?
У меня есть несколько вопросов:
Является ли хорошей идеей создать модель перед написанием кода языка программирования?
Понятно ли мое (ниже) описание проблемы подбрасывания монеты в 30 000 футов?Какие-то детали сбивают с толку?Есть опечатки?
В нижней части этого поста находится модель Alloy, которую я создал.Это понятно?Я показываю два утверждения.Они полезны?Можете ли вы вспомнить другие полезные утверждения?
Вот моя статья:
Лично, прежде чем я реализую программу на каком-то языке программирования, мне хотелось бы получить 30 000Если посмотреть на проблему с ног на голову: мне нравится разбираться в сути проблемы до того, как я завладею особенностями языка программирования.Позвольте мне проиллюстрировать эту перспективу в 30 000 футов на примере броска монеты.
Используется одна монета.Монета имеет два лица, голову и хвост.Вот графическая иллюстрация двух категорий «лица»:
![face category](https://i.stack.imgur.com/kQYu4.gif)
Существует множество подбрасываний монет: {подбрасывание монеты 0, подбрасывание монеты 1, бросок монеты 2,…}
Я сознательно выбрал слово «набор».Я имею в виду «установить» в математическом смысле: нет дубликатов, порядок не имеет значения.Это говорит о том, что при наличии достаточного количества процессоров (или достаточного количества людей) все броски монет могут выполняться параллельно.Порядок бросания монет не имеет значения!
Результатом броска монеты является одно лицо.То есть существует связь между монетой, лицом и броском монеты.
![coin tosses relation](https://i.stack.imgur.com/hxuPW.gif)
Например, предположим, что результат первого броска монеты равенголовы, результатом второго броска монеты являются головы, результатом третьего броска монеты являются хвосты и так далее.Мы можем показать это соотношение в табличной форме:
![instance of coin tosses](https://i.stack.imgur.com/oThV8.gif)
Или в графической форме:
![graphic of coin tosses](https://i.stack.imgur.com/9NIO0.gif)
В отчете о вскрытии (мне просто нравится это слово «посмертно», оно звучит так круто) показано количество подбрасываний монет с головами и количество хвостов.Один прогон из 200 бросков монет привел к этому отчету:
![postmortem report](https://i.stack.imgur.com/LKDhc.gif)
Я думаю, что предыдущее обсуждение довольно хорошо описало суть проблемы:одна монета, есть набор монет, каждый из которых дает голову или хвост, а также отчет о вскрытии, показывающий общее количество голов и хвостов.Это модель проблемы.Существует множество языков для выражения моделей, но мне особенно нравятся Alloy от MIT.Это не только язык моделирования, но и инструмент.С Alloy мы можем не только создать модель, но и исследовать модель, исследуя ее свойства.Что я имею в виду под «собственностью»?Хорошо, вот свойство, которое было бы интересно исследовать: может ли набор бросков монеты дать все головы (или все хвосты)?С Alloy мы выражаем это как утверждение:
Утверждение: отчет о вскрытии никогда не будет содержать всех голов и хвостов.
Мы можем запустить инструмент Alloy, и он будетпоиск контрпримеров.Я запустил Alloy, и он нашел этот контрпример:
![all heads](https://i.stack.imgur.com/fJDVH.gif)
Ах, это возможно возможноза набор бросков монет, чтобы сдать все головы!(Маловероятно, возможно, но возможно)
Мы также хотели бы проверить правильность модели:
Утверждение: количество голов в отчете о смерти после смерти плюс количество хвостовравно количеству брошенных монет.
В этом случае Alloy не находит контрпримеров.Это хорошо.Это дает нам большую уверенность в том, что модель верна (и наше понимание проблемы верно).
Хорошо, теперь я чувствую, что у меня есть четкое понимание проблемы и свойств, которые должна иметь реализация.Я готов реализовать его на языке программирования, таком как Java.
.,,,,,,.
Некоторые из вас могут заинтересоваться моделью Alloy.Я показываю это ниже.Как я уже говорил, мне очень нравится Alloy.Одной из причин является его фундамент в математической теории множеств.Математики изучали наборы в течение тысяч лет, поэтому у Alloy действительно прочная основа.Вот модель Alloy для задачи подбрасывания монеты:
open util/ordering[Coin_Toss]
one sig Coin {
tosses: Face one -> Coin_Toss
}
sig Coin_Toss {}
enum Face { Heads, Tails }
one sig Report {
numHeads: Int,
numTails: Int
}
pred init [c: Coin] {
Coin.tosses.first = Heads or Coin.tosses.first = Tails
}
pred postmortem [c: Coin] {
Report.numHeads = #c.tosses[Heads]
Report.numTails = #c.tosses[Tails]
}
pred coin_tosses {
init [Coin]
all t: Coin_Toss - first |
Coin.tosses.t = Heads or Coin.tosses.t = Tails
postmortem [Coin]
}
run coin_tosses for 200 but 10 Int
assert Not_all_heads {
coin_tosses =>
Report.numTails != 0
}
check Not_all_heads for 200 but 10 Int
assert Num_heads_plus_tails_equals_num_Coin_Toss {
coin_tosses =>
add[Report.numHeads, Report.numTails] = #Coin_Toss
}
check Num_heads_plus_tails_equals_num_Coin_Toss for 50 but 7 Int