Pertanyaan Notasi matematis dari konsep pemrograman


Ada banyak metode untuk merepresentasikan struktur program (seperti diagram kelas UML, dll.). Saya tertarik jika ada konvensi yang menggambarkan program dengan cara matematis yang ketat. Saya terutama tertarik pada penggunaan notasi matematika untuk tujuan ini.

Sebuah contoh: Kelas diwakili sebagai set (bidang, properti) dan fungsi (beroperasi pada elemen set). Bidang kelas induk adalah bagian dari kelas anak. Fungsi dijelaskan dalam pseudocode yang harus terlihat seperti ini dan itu ...


4
2017-10-27 18:31


asal


Jawaban:


Saya tahu bahwa Notasi Z telah digunakan sampai batas tertentu dalam verifikasi formal perangkat lunak, seperti proyek Tokeneer.

Z Notasi

Z Reference Manual


2
2017-10-27 18:41



http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/dp/0201558025


2
2017-10-27 19:33



Ya ada, Logika Floyd-Hoare.


1
2017-10-27 18:36



Ada banyak cara, tetapi saya pikir kebanyakan dari mereka tidak nyaman untuk mengekspresikan struktur karena strukturnya sering tidak dapat diekspresikan dalam konsep matematika default. Pengecualian utama adalah tentu saja bahasa pemrograman fungsional. Pikirkan tentang lipatan (catamorphisme), kelompok, aljabar dll.

Untuk pemrograman imperatif saya tahu keberadaan Z, yang menggunakan kalkulus teori lambda set (murni dan diperpanjang) dan logika predikat (urutan pertama). Namun, saya tidak berpikir itu sangat nyaman. Satu-satunya keuntungan menggunakan matematika untuk mengekspresikan struktur adalah kenyataan bahwa Anda dapat membuktikan hal-hal tentang hal itu. Tetapi jika Anda ingin melakukan itu, lihatlah JML, Spec # atau Eiffel.


1
2017-10-27 18:37



Tergantung pada apa yang ingin Anda capai, tetapi menuruni jalan ini dengan bahasa tertentu dapat membuat Anda mendapat masalah.

Misalnya, lihat diskusi lingkaran-elips pada C ++ FAQ Lite.


1
2017-10-27 18:38



Buku ini menerapkan metode deduktif   untuk pemrograman dengan program afiliasi   dengan matematika abstrak   teori yang memungkinkan mereka bekerja. [...]

aku percaya itu Elemen Pemrograman oleh Alexander Stepanov dan Paul McJones, cukup dekat dengan apa yang Anda cari.

Konsep

Konsep adalah deskripsi   persyaratan pada satu atau lebih jenis   dinyatakan dalam hal keberadaan dan   sifat prosedur, jenis   atribut, dan fungsi-fungsi jenis yang ditentukan   pada jenisnya.


1
2017-10-27 18:47



Z, yang sudah disebutkan, adalah apa yang Anda jelaskan. Ada beberapa varian untuk pemodelan berorientasi objek, tapi saya pikir Anda bisa mendapatkan cukup jauh dengan skema "standar Z" jika Anda ingin memodelkan kelas.

Ada juga Paduan, yang lebih baru dan terinspirasi oleh Z. Notasinya mungkin sedikit lebih dekat dengan orientasi objek. Hal ini juga dapat dianalisis, yaitu Anda dapat memeriksa model yang Anda buat apakah mereka memenuhi persyaratan tertentu, tetapi tidak dapat membuktikan bahwa properti tersebut bertahan, hanya mencoba untuk membantah dalam lingkup terbatas.

Artikel Perangkat Lunak yang Dapat Diandalkan oleh Desain adalah pengantar yang bagus untuk Alloy dan sejenisnya, bersama dengan tabel alat serupa yang tersedia.


1
2017-10-27 19:43



Anda sedang mencari pemrograman fungsional. Ada beberapa bahasa pemrograman fungsional, dan semuanya didasarkan pada teori matematika fundamental yang disebut Kalkulus Lambda. Program yang ditulis dalam bahasa pemrograman fungsional seperti LISP adalah representasi matematis dari diri mereka sendiri. ;-)


1
2018-01-08 16:15



Ada bahasa matematika yang sebenarnya menggambarkan suatu program atau lebih tepatnya operasinya. Anda mengambil keadaan awal dan kemudian mengubah keadaan ini sampai Anda mencapai kondisi target yang diinginkan. Transformasi menghasilkan kode program yang harus dijalankan.

Lihat Artikel Wikipedia tentang logika Hoare.

Ide dasarnya adalah bahwa untuk setiap fungsi (tidak masalah jika Anda memasukkannya ke dalam kelas atau ke fungsi gaya lama), Anda memiliki pra-dan pasca-kondisi. Misalnya, prakondisi dapat berupa bahwa Anda memiliki larik yang memiliki >= 0 elemen. post-condition adalah bahwa setiap elemen [i] harus oleh <= element [j] untuk setiap i <= j.

Deskripsi yang biasa akan "fungsi macam array". Tetapi istilah matematika memungkinkan Anda untuk mengubah input (yang harus sesuai dengan prekondisi) ke dalam output (yang harus sesuai dengan postcondition).

Ini agak berat untuk digunakan, terutama untuk program yang lebih kompleks tetapi beberapa contohnya cukup mengesankan. Seringkali, Anda mendapatkan kode yang benar-benar kompak sebagai hasil yang terlihat cukup rumit tetapi bekerja pada percobaan pertama.


0
2017-10-27 18:47



Saya ingin menyarankan Aljabar Pemrograman. Ini adalah pendekatan perhitungan untuk program, menggunakan Aljabar Relasional, dan Koneksi Galois.

Jika Anda memiliki minat lebih lanjut tentang topik ini, Anda dapat menemukan kertas yang luar biasa, sini, oleh Shin-Cheng Mu, dan José Nuno Oliveira (slide).

Menggunakan Relational Aljabar dan First-Order Logic, juga memiliki sinergi yang bagus dengan Paduan, Pemrograman Fungsional, dan Desain dengan Kontrak (mudah diterapkan pada Pemrograman Berorientasi Objek).


0
2018-02-24 02:07